通过突变、动态分析和静态检查推断循环不变量
Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking
摘要：
验证器可以证明程序正确的对他们的全部功能规格要求，为程序与循环，额外的注释形式的循环不变量-属性，保持每次迭代的循环。我们表明，显着的循环不变的候选人可以通过系统地突变后置条件，然后，动态检查（基于自动生成的测试）淘汰无效的候选人，和静态检查选择可证明有效的。我们提出了一个自动应用这些技术来支持程序证明器的框架，为无需手动编写循环不变式的全自动验证铺平了道路：适用于28种方法（包括39个不同的循环）从不同的java.util类（偶尔修改，以避免使用静态检查器不完全支持的Java功能），我们的EQUIPATE原型自动履行了97%的证明义务，这导致了28种方法中的25种的自动完全正确性证明-优于用于全自动验证的几种最先进的工具。
英文摘要：
Verifiers that can prove programs correct against their full functional specification require, for programs with loops, additional annotations in the form of loop invariants---propeties that hold for every iteration of a loop. We show that significant loop invariant candidates can be generated by systematically mutating postconditions; then, dynamic checking (based on automatically generated tests) weeds out invalid candidates, and static checking selects provably valid ones. We present a framework that automatically applies these techniques to support a program prover, paving the way for fully automatic verification without manually written loop invariants: Applied to 28 methods (including 39 different loops) from various java.util classes (occasionally modified to avoid using Java features not fully supported by the static checker), our DYNAMATE prototype automatically discharged 97% of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods---outperforming several state-of-the-art tools for fully automatic verification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
