Automatic Abstraction in SMT-Based Unbounded Software Model Checking

TL;DR

This paper introduces an automatic abstraction method integrated with SMT-based unbounded software model checking, enhancing verification efficiency through proof and counterexample-based refinement, and demonstrates its effectiveness on challenging benchmarks.

Contribution

It is the first to adapt Proof-Based Abstraction for software verification, combining it with under-approximation techniques in a unified iterative framework.

Findings

Effective on hard verification benchmarks

Combines proof-based and counterexample-based abstraction

Prototype implemented with Z3 SMT solver

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.