Interpolation-based model checking (McMillan, 2003) is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. 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. This paper closes this significant, 19 years 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 over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.
翻译:基于内插的模型检查(McMillan,2003年)是一种正式的核查算法,最初是为了核查有限状态过渡系统的安全性而设计的。算法是硬件模型检查中最先进的算法。它从无法满足的BMC查询中获取了中间线,收集了它们来构建一套过分一致的可达状态。不同于其他正式核查算法,如K-imging或PDR,这些算法已经扩展用于处理无限状态系统,并被调查用于方案分析。McMilllan2003年基于内插的模型核对算法至今尚未用于核查程序。这份文件通过采用软件核查算法,弥补了19年来在知识方面的这一重大差距。我们在核查框架ACP校验器中应用了它,对照其他最先进的软件验证技术,例如K-iming或PDR。评价表明,基于内插法的模型核对方法在目前解决核查任务的数量方面与其他算法相比,具有竞争性。我们选择了重要的核查方法,因为开发者们可能选择了较先进的方法。