Faculty of Information Technology, BUT

Publication Details

Accelerating Interpolants

IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor and RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science, vol. 2012, no. 7561, pp. 187-202. ISSN 0302-9743.
Czech title
Akcelerované interpolanty
Type
journal article
Language
english
Authors
Iosif Radu (VERIMAG)
Hojjat Hossein (EPFL)
Konečný Filip, Ing. (DITS FIT BUT)
Kuncak Viktor (EPFL)
Rummer Philipp (Uppsala)
Keywords
integer programs, verification, reachability analysis, acceleration, predicate abstraction, interpolation
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.
Published
2012
Pages
187-202
Journal
Lecture Notes in Computer Science, vol. 2012, no. 7561, ISSN 0302-9743
Book
Proceedings of ATVA'12
Publisher
Springer Verlag
BibTeX
@ARTICLE{FITPUB10102,
   author = "Radu Iosif and Hossein Hojjat and Filip Kone\v{c}n\'{y} and Viktor Kuncak and Philipp Rummer",
   title = "Accelerating Interpolants",
   pages = "187--202",
   booktitle = "Proceedings of ATVA'12",
   journal = "Lecture Notes in Computer Science",
   volume = 2012,
   number = 7561,
   year = 2012,
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10102"
}
Back to top