Augmenting Interpolation-Based Model Checking with Auxiliary Invariants
This work is accepted at SPIN 2024
and won the Best Paper Award.
A 
preprint,
the 
publisher's version,
and an 
extended technical report
of the article are available for you to download.
Abstract
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.
Reproduction Information
A reproduction package of this work is available on Zenodo
(
).
It was reviewed by the Artifact Evaluation Committee at SPIN 2024 and awarded the (Functional and) Reusable and Available badges.
The 
SVN repository
(corresponding 
git commit)
contains the revision of CPAchecker used in the evaluation.
Experimental Results
The experimental results reported in the paper can be viewed in the interactive tables linked below. You can click on the cells in the status columns to see the respective log output and navigate through the tabs to view various plots.- 10 selected tasks where IMCi←DF demonstrates significant improvement over plain IMC
- 10 selected tasks where IMCf←DF demonstrates significant improvement over plain IMC
- Plain vs. augmented IMC on 870 tasks with non-trivial auxiliary invariants
- Plain IMC vs. IMCi←DF on 870 tasks with non-trivial auxiliary invariants using different random seeds for SMT solving
- IMCi←DF vs. other algorithms and verifiers on 1623 difficult verification tasks