Meta-F*：结合 SMT、策略与元程序的证明自动化
编程语言
2019-03-08 v4 计算机科学中的逻辑
摘要
我们介绍了 Meta-F*，一个用于 F* 程序验证器的策略与元编程框架。Meta-F* 的主要创新在于允许使用策略和元编程来处理 SMT 无法求解的断言，或者仅将其简化为良态的 SMT 片段。此外，Meta-F* 可用于自动生成已验证的代码。Meta-F* 被实现为一种 F* 效应，鉴于 F* 强大的效应系统，这极大地增加了代码重用，甚至实现了元程序的轻量级验证。元程序可以被解释执行，也可以编译为高效的原生代码，动态加载到 F* 类型检查器中，并与解释执行的代码互操作。在真实案例研究上的评估表明，Meta-F* 在证明开发、效率和鲁棒性方面提供了显著的收益。
引用
@article{arxiv.1803.06547,
title = {Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms},
author = {Guido Martínez and Danel Ahman and Victor Dumitrescu and Nick Giannarakis and Chris Hawblitzel and Catalin Hritcu and Monal Narasimhamurthy and Zoe Paraskevopoulou and Clément Pit-Claudel and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy},
journal= {arXiv preprint arXiv:1803.06547},
year = {2019}
}
备注
Full version of ESOP'19 paper