Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification

Dirk Beyer, Nian-Ze Lee, and Philipp Wendler

A preprint of this article (also on arXiv DOI) is available for you to download. This work was presented at iPRA 2022 (slides).


Abstract

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.


Reproduction Information

The full reproduction package is available at Zenodo (DOI). The SVN repository contains the revision of CPAchecker used in the evaluation. The benchmark set can be downloaded from the SV-COMP repository.


Full Results

This table contains the full results of all algorithms evaluated in the paper. You can click on the cells in the status columns to see the respective log output and use the respective tabs to show various plots, e.g., a quantile plot.