通过变异、动态分析和静态检查推断循环不变量
软件工程
2016-02-09 v4
摘要
能够针对完整功能规范证明程序正确性的验证器，对于包含循环的程序，需要以循环不变量（即在循环的每次迭代中都成立的属性）形式的额外注释。我们展示了可以通过系统地变异后置条件来生成重要的循环不变量候选；然后，动态检查（基于自动生成的测试）剔除无效候选，而静态检查则选择可证明有效的候选。我们提出了一个自动应用这些技术以支持程序证明器的框架，为无需手动编写循环不变量的全自动验证铺平了道路：将该方法应用于来自各种 java.util 类的 28 个方法（包括 39 个不同的循环，偶尔经过修改以避免使用静态检查器未完全支持的 Java 特性），我们的 DYNAMATE 原型自动解除了 97% 的所有证明义务，从而实现了 28 个方法中 25 个的自动完全正确性证明，优于几种用于全自动验证的最先进工具。
引用
@article{arxiv.1407.5286,
title = {Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking},
author = {Juan P. Galeotti and Carlo A. Furia and Eva May and Gordon Fraser and Andreas Zeller},
journal= {arXiv preprint arXiv:1407.5286},
year = {2016}
}
备注
Only change in v4: rectified May's affiliation