使用 Boogie 验证 Eiffel 程序
软件工程
2011-06-24 v1
摘要
Spec#、Dafny、jStar 和 VeriFast 等静态程序验证器代表了自动化功能验证技术的最新水平。下一个公开挑战是使验证工具即使对于不精通形式化技术的程序员也能使用。本文介绍了 AutoProof，一个将 Eiffel 程序翻译为 Boogie 并使用 Boogie 验证器加以证明的验证工具。为了能够用于真实程序，AutoProof 完全支持多种高级面向对象特性，包括多态、继承和函数对象。AutoProof 还采用简单策略来减少验证程序时所需的注解数量（例如框架条件）。本文阐述了 AutoProof 翻译的主要特性，包括一些正在实现中的特性，并通过示例和案例研究进行了演示。
引用
@article{arxiv.1106.4700,
title = {Verifying Eiffel Programs with Boogie},
author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
journal= {arXiv preprint arXiv:1106.4700},
year = {2011}
}
备注
Accepted at BOOGIE 2011