Accelerating Interpolants

paper ps   
We present Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR), a new algorithm for verifying infinite-state transition systems. CEGAAR combines interpolation-based predicate discovery in counterexample-guided predicate abstraction with acceleration technique for computing the transitive closure of loops. CEGAAR applies acceleration to dynamically discovered looping patterns in the unfolding of the transition system, and combines overapproximation with underapproximation. It constructs inductive invariants that rule out an infinite family of spurious counterexamples, alleviating the problem of divergence in predicate abstraction without losing its adaptive nature. We present theoretical and experimental justification for the effectiveness of CEGAAR, showing that inductive interpolants can be computed from classical Craig interpolants and transitive closures of loops. We present an implementation of CEGAAR that verifies integer transition systems. We show that the resulting implementation robustly handles a number of difficult transition systems that cannot be handled using interpolation-based predicate abstraction or acceleration alone.

Citation

Hossein Hojjat, Radu Iosif, Filip Konečný, Viktor Kuncak, and Philipp Rümmer. Accelerating interpolants. In Automated Technology for Verification and Analysis (ATVA), 2012.

BibTex Entry

@inproceedings{HojjatETAL12AcceleratingInterpolants,
  author = {Hossein Hojjat and Radu Iosif and
  Filip Kone\v{c}n\'{y} and Viktor Kuncak and Philipp R\"ummer},
  title = {Accelerating Interpolants},
  booktitle = {Automated Technology for Verification and Analysis (ATVA)},
  year = 2012,
  abstract = {We present Counterexample-Guided Accelerated Abstraction
Refinement (CEGAAR), a new algorithm for verifying infinite-state
transition systems.  CEGAAR combines interpolation-based predicate 
discovery in counterexample-guided predicate abstraction with
acceleration technique for computing the transitive closure of
loops. CEGAAR applies acceleration to dynamically discovered
looping patterns in the unfolding of the transition system, and
combines overapproximation with underapproximation. It constructs
inductive invariants that rule out an infinite family of spurious
counterexamples, alleviating the problem of divergence in predicate
abstraction without losing its adaptive nature. We present theoretical
and experimental justification for the effectiveness of CEGAAR,
showing that inductive interpolants can be computed from classical
Craig interpolants and transitive closures of loops. We present an
implementation of CEGAAR that verifies integer transition
systems. We show that the resulting implementation robustly handles a
number of difficult transition systems that cannot be handled using
interpolation-based predicate abstraction or acceleration alone.}
}