An abstraction refinement approach combining precise and approximated techniques

Keywords:

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 a given set of predicates. A precise abstraction contains the minimal set of transitions with regard to the predicates, 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 paper proposes a new approach that employs both precise (slow) and approximated (fast) abstraction techniques within one abstraction-refinement loop. 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 almost systematically outperforms both precise and imprecise techniques.

• BibTex

@article { Natasha Sharygin,
	title = {An abstraction refinement approach combining precise and approximated techniques},
	journal = {International Journal on Software Tools for Technology Transfer (STTT)},
	volume = {14},
	year = {2012},
	pages = {1-14},
	publisher = {Springer},
	keywords = {Predicate abstraction, Precise abstraction, Approximated abstraction, CEGAR},
	URL = {http://dx.doi.org/10.1007/s10009-011-0185-y},
	author = {Natasha Sharygina and  Stefano Tonetta and  Aliaksei Tsitovich}
}