Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.

翻译：软件模型检测是一个具有挑战性的问题，生成相关不变量是证明程序安全属性的关键因素。程序不变量可通过多种方法获取，包括基于数据流分析的轻量级程序和利用Craig插值的高开销技术。虽然数据流分析运行高效，但其生成的不变量往往过于薄弱而无法证明安全属性。相比之下，基于插值的方法能从插值结果构建强不变量，但昂贵的插值过程可能导致可扩展性不足。不变量也可注入模型检测算法以辅助分析。不变量注入已在多种知名方法中得到研究，包括k-归纳法、谓词抽象和符号执行。我们提出了一种增强型基于插值的验证算法，将外部不变量注入基于插值的模型检测（McMillan, 2003）——这种硬件模型检测算法近期被应用于软件验证。辅助不变量有助于剪枝Craig插值中的不可达状态，并将分析限定在程序的可达部分。我们在验证框架CPAchecker中实现了所提技术，并对其与CPAchecker中成熟的基于SMT的方法以及其他先进软件验证器进行了评估。实验发现，注入不变量能减少证明安全属性所需的插值查询次数并提升运行时效率。因此，所提出的不变量注入方法验证了其朴素版本（即不含不变量）、不变量生成器或任何对比工具均无法解决的困难任务。