# Automatic Abstraction in SMT-Based Unbounded Software Model Checking

arXiv: https://arxiv.org/abs/1306.1945 · HTML: https://mlsanity.com/paper/1306.1945/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Jun 2013.

## Built on by (most cited first, 1 of 1)

- [Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning](https://mlsanity.com/paper/2305.01206/) (2023)

## Abstract (arXiv)

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.