The Synergy of Precise and Fast Abstractions for Program Verification
It produces a conservative over-approximation where concrete states are grouped together according to the predicates.
- Starts at
TU Wien, Campus Favoritenstraße
1040 Vienna, Favoritenstraße 9-11
Stiege 1, 3. Stock, Gelber Bereich
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.
- Natasha Sharygina, University of Lugano, Switzerland and Carnegie Mellon University, USA
Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!