Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikačního výsledku
IOSIF, R.; HOJJAT, H.; KONEČNÝ, F.; KUNCAK, V.; RUMMER, P.
Originální název
Accelerating Interpolants
Anglický název
Druh
Článek recenzovaný mimo WoS a Scopus
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
Klíčová slova
integer programs, verification, reachability analysis, acceleration, predicate abstraction, interpolation
Klíčová slova v angličtině
Autoři
Rok RIV
2013
Vydáno
31.07.2012
Nakladatel
Springer Verlag
Kniha
Proceedings of ATVA'12
ISSN
0302-9743
Periodikum
Lecture Notes in Computer Science
Svazek
2012
Číslo
7561
Stát
Spolková republika Německo
Strany od
187
Strany do
202
Strany počet
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" }