Translating Scala Programs to Isabelle/HOL
Proceedings of the 8th International Joint Conference on Automated Reasoning - Volume 9706(2016)
摘要
We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs) stemming from the input program. Isabelle, on the other hand, is an interactive theorem prover used to verify mathematical specifications using its own input language Isabelle/Isar. Users specify (inductive) definitions and write proofs about them manually, albeit with the help of semi-automated tactics. The integration of these two systems allows us to exploit Isabelle’s rich standard library and give greater confidence guarantees in the correctness of analysed programs.
更多查看译文
关键词
Isabelle,HOL,Scala,Leon,Compiler
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要