Detail publikace

Accelerating Interpolants

Originální název

Accelerating Interpolants

Anglický název

Accelerating Interpolants

Jazyk

en

Originální abstrakt

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.

Anglický abstrakt

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.

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"
}