uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Accelerating interpolants
Show others and affiliations
2012 (English)In: Automated Technology for Verification and Analysis: 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings, 2012, 187-202 p.Conference paper, Published paper (Refereed)
Abstract [en]

We present Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR), a new algorithm for verifying infinite-state transition systems. CEGAAR combines interpolation-based predicate discovery in counterexample-guided 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.

Place, publisher, year, edition, pages
2012. 187-202 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7561
National Category
Natural Sciences
Identifiers
URN: urn:nbn:se:uu:diva-186815DOI: 10.1007/978-3-642-33386-6_16ISBN: 978-3-642-33385-9 (print)OAI: oai:DiVA.org:uu-186815DiVA: diva2:576053
Conference
10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012, 3 October 2012 through 6 October 2012, Thiruvananthapuram, India
Projects
UPMARC
Available from: 2012-12-12 Created: 2012-11-29 Last updated: 2017-01-19

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Rümmer, Phillipp

Search in DiVA

By author/editor
Rümmer, Phillipp
By organisation
Computer Systems
Natural Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 401 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf