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.
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants
Lect.Notes Computer
International Symposium on Model Checking Software ; 2024 ; Luxembourg City, Luxembourg April 10, 2024 - April 11, 2024
13.10.2024
21 pages
Aufsatz/Kapitel (Buch)
Elektronische Ressource
Englisch
Software model checking , Program invariants , Invariant injection , Craig interpolation , Data-flow analysis , SMT , SAT Engineering , Control, Robotics, Mechatronics , Software Engineering/Programming and Operating Systems , Artificial Intelligence , Computer Systems Organization and Communication Networks , Computer Science
British Library Online Contents | 1996
|NTIS | 1975
|Auxiliary device for checking green channel of highway toll station
Europäisches Patentamt | 2024
|NTIS | 1981
|