与Dafny一起开发可达性评估验证程序的案例研究
Case studies of development of verified programs with Dafny for accessibility assessment
摘要：
形式化验证技术旨在形式化地证明计算机程序相对于形式规范的正确性，但是应用形式规范和验证技术所需的专业知识和努力以及可扩展性问题限制了它们的实际应用。近年来，SAT和SMT求解器的巨大进步使得新一代工具的构建成为可能，这些工具通过自动化大多数（如果不是全部）验证过程，使形式化验证更容易为软件工程师所用。Dafny系统是这一趋势的一个突出例子。然而，关于其可获得性的证据很少。为了帮助填补这一空白，我们进行了一组10个案例研究，在Dafny中开发一些真实世界的算法和数据结构的验证实现，以确定其对软件工程师的可访问性。我们发现，平均而言，为规范和验证目的编写的代码数量与为实现和测试目的编写的传统代码数量级相同（比率为1.14）-对于高完整性软件来说，这无疑是一项“开销”。Dafny验证器的性能令人印象深刻，每行代码生成2.4个证明义务，平均每个证明义务生成和验证花费24 ms。但是，我们也发现，编写辅助验证码所需的手工工作可能是显著的，并且难以预测和掌握。因此，核查任务的进一步自动化和系统化是这一领域未来发展的可能方向。
英文摘要：
Formal verification techniques aim at formally proving the correctness of a computer program with respect to a formal specification, but the expertise and effort required for applying formal specification and verification techniques and scalability issues have limited their practical application. In recent years, the tremendous progress with SAT and SMT solvers enabled the construction of a new generation of tools that promise to make formal verification more accessible for software engineers, by automating most if not all of the verification process. The Dafny system is a prominent example of that trend. However, little evidence exists yet about its accessibility. To help fill this gap, we conducted a set of 10 case studies of developing verified implementations in Dafny of some real-world algorithms and data structures, to determine its accessibility for software engineers. We found that, on average, the amount of code written for specification and verification purposes is of the same order of magnitude as the traditional code written for implementation and testing purposes (ratio of 1.14) -- an ``overhead'' that certainly pays off for high-integrity software. The performance of the Dafny verifier was impressive, with 2.4 proof obligations generated per line of code written, and 24 ms spent per proof obligation generated and verified, on average. However, we also found that the manual work needed in writing auxiliary verification code may be significant and difficult to predict and master. Hence, further automation and systematization of verification tasks are possible directions for future advances in the field.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
