Publication result detail

Accelerating Interpolants

IOSIF, R.; HOJJAT, H.; KONEČNÝ, F.; KUNCAK, V.; RUMMER, P.

Original Title

Accelerating Interpolants

English Title

Accelerating Interpolants

Type

Peer-reviewed article not indexed in WoS or Scopus

Original 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 counterexampleguided 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.

English 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 counterexampleguided 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.

Keywords

integer programs, verification, reachability analysis, acceleration, predicate abstraction, interpolation

Key words in English

integer programs, verification, reachability analysis, acceleration, predicate abstraction, interpolation

Authors

IOSIF, R.; HOJJAT, H.; KONEČNÝ, F.; KUNCAK, V.; RUMMER, P.

RIV year

2013

Released

31.07.2012

Publisher

Springer Verlag

Book

Proceedings of ATVA'12

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Volume

2012

Number

7561

State

Federal Republic of Germany

Pages from

187

Pages to

202

Pages count

16

BibTex

@article{BUT97017,
  author="Iosif {Radu} and Hossein {Hojjat} and Filip {Konečný} and Viktor {Kuncak} and Philipp {Rummer}",
  title="Accelerating Interpolants",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7561",
  pages="187--202",
  issn="0302-9743"
}