Title | An abstraction refinement approach combining precise and approximated techniques |
Publication Type | Journal Article |
Year of Publication | 2012 |
Authors | Sharygina, Natasha, Tonetta Stefano, and Tsitovich Aliaksei |
Journal | International Journal on Software Tools for Technology Transfer (STTT) |
Volume | 14 |
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. |
URL | https://link.springer.com/article/10.1007/s10009-011-0185-y |