Publication detail

Accelerating Interpolants

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

Original Title

Accelerating Interpolants

English Title

Accelerating Interpolants

Type

journal article - other

Language

en

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

RIV year

2012

Released

31.07.2012

Publisher

Springer Verlag

Location

NEUVEDEN

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

2012

Number

7561

State

DE

Pages from

187

Pages to

202

Pages count

16

Documents

BibTex


@article{BUT97017,
  author="Iosif {Radu} and Hossein {Hojjat} and Filip {Konečný} and Viktor {Kuncak} and Philipp {Rummer}",
  title="Accelerating Interpolants",
  annote="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.",
  address="Springer Verlag",
  booktitle="Proceedings of ATVA'12",
  chapter="97017",
  edition="NEUVEDEN",
  howpublished="print",
  institution="Springer Verlag",
  number="7561",
  volume="2012",
  year="2012",
  month="july",
  pages="187--202",
  publisher="Springer Verlag",
  type="journal article - other"
}