An abstraction refinement approach combining precise and approximated techniques |
| |
Authors: | Natasha Sharygina Stefano Tonetta Aliaksei Tsitovich |
| |
Affiliation: | (1) Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA;(2) Computer Systems Institute, ETH Zurich, Switzerland |
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|