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. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
 
conference paper

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

Beyer, Dirk
•
Henzinger, Thomas A.  
•
Théoduloz, Grégory  
2007
Computer Aided Verification. CAV 2007
19th International Conference on Computer Aided Verification

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. We designed an algorithm and built a tool that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool take one or more abstract interpreters, such as a predicate abstraction and a shape analysis, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.

  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-540-73368-3_51
Author(s)
Beyer, Dirk
Henzinger, Thomas A.  
Théoduloz, Grégory  
Date Issued

2007

Publisher

Springer

Published in
Computer Aided Verification. CAV 2007
Series title/Series vol.

Lecture Notes in Computer Science; 4590

Start page

504

End page

518

Subjects

Software Model Checking

•

NCCR-MICS

•

NCCR-MICS/CL2

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
MTC  
Event nameEvent placeEvent date
19th International Conference on Computer Aided Verification

Berlin, Germany

July 3-7, 2007

Available on Infoscience
May 1, 2007
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/6444
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