大规模 QED：形式化验证软件工程综述
计算机科学中的逻辑
2020-03-17 v1 编程语言
摘要
开发程序正确性的形式化证明可提高实际与感知的可靠性，并增进对程序规约及其底层假设的理解。支持此类开发的工具已存在 40 余年，但直到最近才得到广泛实际应用。基于机器检查形式化证明构建的项目目前正达到前所未有的规模，可与大型软件项目相比拟，这给证明的开发与维护带来了新挑战。尽管其重要性日益增加，证明工程领域却很少被单独考量；相关理论、技术与工具横跨诸多领域与会议。本综述对文献进行调研，呈现关于程序正确性的证明工程的整体理解，涵盖实际影响、基础、证明自动化、证明组织与实际证明开发。
引用
@article{arxiv.2003.06458,
title = {QED at Large: A Survey of Engineering of Formally Verified Software},
author = {Talia Ringer and Karl Palmskog and Ilya Sergey and Milos Gligoric and Zachary Tatlock},
journal= {arXiv preprint arXiv:2003.06458},
year = {2020}
}
备注
183 pages, for errata see https://proofengineering.org/qed_errata.html