Automatic Abstraction in SMT-Based Unbounded Software Model Checking

摘要

Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e., reachability) properties. They combine two key ideas - (a) concreteness: a counterexample in an under-approximation is a counterexample in the original program as well, and (b) generalization: a proof of safety of an under-approximation, produced by an SMT solver, are generalizable to proofs of safety of the original program. In this paper, we present a combination of automatic abstraction with the under-approximation-driven framework. We explore two iterative approaches for obtaining and refining abstractions - proof based and counterexample based - and show how they can be combined into a unified algorithm. To the best of our knowledge, this is the first application of Proof-Based Abstraction, primarily used to verify hardware, to Software Verification. We have implemented a prototype of the framework using Z3, and evaluate it on many benchmarks from the Software Verification Competition. We show experimentally that our combination is quite effective on hard instances.