The article "Interpolation and SAT-Based Model Checking" (McMillan, 2003) describes a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. It derives interpolants from unsatisfiable BMC queries and collects them to construct an overapproximation of the set of reachable states. Although 20 years old, the algorithm is still state-of-the-art in hardware model checking. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model-checking algorithm from 2003 has not been used to verify programs so far. Our contribution is to close this significant, two decades old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker and evaluated the implementation against other state-of-the-art software-verification techniques on the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that McMillan's interpolation-based model-checking algorithm from 2003 is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results are important for the area of software verification, because researchers and developers now have one more approach to choose from.

翻译：文章《插值与基于SAT的模型检测》（McMillan, 2003）描述了一种形式化验证算法，该算法最初旨在验证有限状态转移系统的安全属性。它从不满足的BMC查询中推导出插值，并收集这些插值以构建可达状态集的超近似。尽管已有20年历史，该算法在硬件模型检测中仍处于领先地位。与k-归纳法或PDR等其他已扩展到处理无限状态系统并用于程序分析的形式化验证算法不同，McMillan于2003年提出的基于插值的模型检测算法至今未用于验证程序。我们的贡献在于通过将该算法应用于软件验证，弥补了这一长达二十年的知识空白。我们在验证框架CPAchecker中实现了该算法，并在最大的公开C语言安全验证任务基准套件上，将其与其他最先进的软件验证技术进行了评估。评估结果表明，McMillan于2003年提出的基于插值的模型检测算法在求解验证任务数量和运行时效率方面均与其他算法具有竞争力。该结果对软件验证领域具有重要意义，因为研究人员和开发者如今又多了一种可供选择的验证方法。