结合k-归纳和连续精化不变量
Combining k-Induction with Continuously-Refined Invariants
摘要：
有界模型检验（BMC）是一种用于发现软件缺陷的著名且成功的技术。k-induction是一种将基于BMC的方法从证伪扩展到验证的方法。自动生成的辅助不变量可以用来加强归纳假设。我们改进了这种方法，并通过以下方式进一步提高了有效性和效率：我们从轻量级不变量开始，并在分析过程中不断完善这些不变量。我们提出并评估我们的方法在开源验证框架CPAchecker的实施。我们的实验表明，将k-归纳法与不断改进的不变量相结合，显着提高了有效性和效率，并在成功的验证结果方面优于所有现有的基于k-归纳法的软件验证实现。
英文摘要：
Bounded model checking (BMC) is a well-known and successful technique for finding bugs in software. k-induction is an approach to extend BMC-based approaches from falsification to verification. Automatically generated auxiliary invariants can be used to strengthen the induction hypothesis. We improve this approach and further increase effectiveness and efficiency in the following way: we start with light-weight invariants and refine these invariants continuously during the analysis. We present and evaluate an implementation of our approach in the open-source verification-framework CPAchecker. Our experiments show that combining k-induction with continuously-refined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of k-induction-based software verification in terms of successful verification results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
