An abstraction refinement approach combining precise and approximated techniques

Publication Type:

Journal Article


Sharygina, N.; Tonetta, S.; Tsitovich, A.


International Journal on Software Tools for Technology Transfer (STTT), Springer, Volume 14, Issue 1, p.1-14 (2012)


Predicate abstraction; Precise abstraction; Approximated abstraction; CEGAR


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.

@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 = {},
	author = {Natasha Sharygina and  Stefano Tonetta and  Aliaksei Tsitovich}

stt11_draft.pdf489.08 KB