Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Accelerating Interpolants
 
conference paper

Accelerating Interpolants

Hojjat, Hossein  
•
Iosif, Radu  
•
Konecny, Filip
Show more
2012
ATVA 2012: Automated Technology for Verification and Analysis
10th International Symposium on Automated Technology for Verification and Analysis

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.

  • Files
  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-33386-6_16
Author(s)
Hojjat, Hossein  
Iosif, Radu  
Konecny, Filip
Kuncak, Viktor  orcid-logo
Rummer, Philipp
Date Issued

2012

Published in
ATVA 2012: Automated Technology for Verification and Analysis
Start page

187

End page

202

Subjects

Predicate Abstraction

•

Loop Acceleration

•

Interpolation

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Event nameEvent placeEvent date
10th International Symposium on Automated Technology for Verification and Analysis

Thiruvananthapuram, India

October 3-6, 2012

Available on Infoscience
August 15, 2012
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/84602
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés