@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 = {Approximated abstraction, CEGAR, Precise abstraction, Predicate abstraction},
	url = {http://dx.doi.org/10.1007/s10009-011-0185-y},
	author = {Natasha Sharygina and Tonetta, S. and Tsitovich, A.}
}
@article {340,
	title = {An abstraction refinement approach combining precise and approximated techniques},
	journal = {International Journal on Software Tools for Technology Transfer (STTT)},
	volume = {14},
	year = {2012},
	abstract = {<p>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.</p>
},
	url = {https://link.springer.com/article/10.1007/s10009-011-0185-y},
	author = {Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich}
}
