发表机构
University of Michigan（密歇根大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出ProofSaX工具，通过将大型验证任务分片并独立探索证明搜索空间，减少人工干预，以自动化合成分布式系统的正确性证明，并在103个任务中成功完成86个。
AI 中文摘要
分布式系统难以正确实现，且使用传统测试可能无法检测到细微的缺陷。形式化验证为证明复杂分布式系统的正确性提供了一种替代方案。尽管先前已有自动化和促进形式化验证的努力，但将形式化验证集成到软件开发中仍然困难。程序员需要反复查询定理证明器以找到其系统的正确证明。这种与定理证明器反复交互的过程涉及大量人工干预，成为在软件开发中采用形式化验证的障碍。在本文中，我们通过减少寻找分布式系统正确性证明所需的人工干预，来解决在实践中扩展形式化验证的挑战。我们提出了ProofSaX，一种自动化工具，它将大型验证任务分片，并独立探索每个分片的证明搜索空间以合成正确性证明。我们在添加可能的证明注释时使用受控探索来处理搜索空间爆炸问题。我们在分布式系统的各种安全性证明上评估了ProofSaX。我们表明，在103个证明完成任务中，ProofSaX能够在86个任务中找到最后一个证明注释，运行时间从一分钟到两小时不等。
英文摘要
Distributed systems are hard to implement correctly, and subtle bugs can go undetected using traditional testing. Formal verification offers an alternative for proving the correctness of complex distributed systems. Despite previous efforts to automate and facilitate formal verification, it is still hard to integrate formal verification in software development. Programmers need to query the theorem prover repeatedly to find the correct proof of their system. This cycle of going back and forth with the theorem prover involves a lot of human intervention and is a barrier to adopting formal verification in software development. In this paper, we address the challenges of scaling formal verification in practice by reducing the human intervention required to find the correctness proof of a distributed system. We propose ProofSaX, an automated tool that shards large verification tasks and explores the proof search space for each shard independently to synthesize correctness proofs. We use controlled exploration when adding possible proof annotations to handle the search-space explosion problem. We evaluate ProofSaX on a variety of safety proofs for distributed systems. We show that ProofSaX can find the last proof annotation in 86 out of 103 proof-completion tasks, with runtimes ranging from one minute to two hours.
