Automatic Abstraction in SMT-Based Unbounded Software Model Checking

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund Clarke, Proceedings of the 25th International Conference on Computer Aided Verification (CAV), page 846-862, July 13-19, 2013, St. Petersburg, Russia.

Abstract: 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.

Online