Informatics, TU Vienna

The Synergy of Precise and Fast Abstractions for Program Verification

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.

Abstract

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 it 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.

In this talk I will present 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 software model checker. Our tests with various real life benchmarks show that the new approach systematically outperforms the classical approaches based on precise and imprecise techniques.

This is a joint work with my students, Aliaksei Tsitovich and Stefano Tonetta.