Meta-F \star - Proof Automation with SMT, Tactics, and Metaprograms.
arXiv: Programming Languages(2019)
摘要
We introduce Meta-F-star, a tactics and metaprogramming framework for the F-star program verifier. The main novelty of Meta-F-star is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F-star can be used to generate verified code automatically. Meta-F-star is implemented as an F-star effect, which, given the powerful effect system of F-star, heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F-star type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F-star provides substantial gains in proof development, efficiency, and robustness.
更多查看译文
关键词
Tactics, Metaprogramming, Program verification, Verification conditions, SMT solvers, Proof assistants
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要