QED at Large: A Survey of Engineering of Formally Verified Software
QED at Large: A Survey of Engineering of Formally Verified Software
复制标题
DOI：
10.1561/2500000045
复制
发表时间：
2019-09
期刊：
影响因子：
--
通讯作者：
T. Ringer;Karl Palmskog;Ilya Sergey;Miloš Gligorić;Zachary Tatlock
中科院分区：
文献类型：
--
作者：
T. Ringer;Karl Palmskog;Ilya Sergey;Miloš Gligorić;Zachary Tatlock
制定计划正确性的正式证明可以提高实际和可感知的可靠性，并促进对程序规范及其基本假设的更好理解。支持这种开发的工具已有40多年的历史，但直到最近才看到广泛的实际用途。基于机器检查正式证明的建设的项目现在已经达到了前所未有的规模，可与大型软件项目相当，这导致了证明开发和维护方面的新挑战。尽管其重要性越来越大，但很少考虑证明工程领域。相关的理论，技术和工具涵盖了许多领域和场地。对文献的调查对证明工程的完整理解了程序的正确性，涵盖了实践，基础，证明自动化，证明组织和实际证明开发的影响。
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have been available for over 40 years, but have only recently seen wide practical use. Projects based on construction of machine-checked formal proofs are now reaching an unprecedented scale, comparable to large software projects, which leads to new challenges in proof development and maintenance. Despite its increasing importance, the field of proof engineering is seldom considered in its own right; related theories, techniques, and tools span many fields and venues. This survey of the literature presents a holistic understanding of proof engineering for program correctness, covering impact in practice, foundations, proof automation, proof organization, and practical proof development.