Software Model Checking via Iterative Abstraction Refinement of Constraint Logic Queries
Cormac Flanagan · 2007
Abstract. Existing predicate abstraction tools rely on both theorem provers (to abstract the original program) and model checkers (to check the abstract program). This paper combines these theorem proving and model checking components in a unified algorithm. The correctness of the original, infinite-state program is expressed as a single query in constraint logic, which is sufficiently expressive to encode recursion and least fixed-point computations. The satisfiability of this query is decided using a combination of predicate abstraction, counterexample-based predicate inference, and proof-based explication. Our algorithm avoids the Cartesian approximation while reducing the number of theorem prover queries. 1