Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to the predicates. Given a set of predicates, a precise abstraction contains the minimal set of transitions, but as a result is computationally expensive. Most model checkers, therefore, approximate the abstraction to alleviate the computation of the abstract system by trading off precision with cost. However, approximation results in a higher number of refinement iterations, since it can produce more false counterexamples than its precise counterpart. The refinement loop can become prohibitively expensive for large programs.
This project proposes a new abstraction refinement technique that combines slow and precise predicate abstraction techniques with fast and imprecise ones. It allows computing the abstraction quickly but keeps it precise enough to avoid too many refinement iterations. We implemented the new algorithm in a state-of-the-art software model checker. Our tests with various real-life benchmarks show that the new approach systematically outperforms both precise and imprecise techniques.
The results were published in [1]. The benchmarks and binaries we used for evaluation are available.
References
- The Synergy of Precise and Fast Abstractions for Program Verification, , 24th Annual ACM Symposium on Applied Computing (SAC), Honolulu, USA, p.566-573, ACM (2009)
