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

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.


Publié dans:
Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007, Berlin, Germany, July 3-7), 504-518
Présenté à:
Computer Aided Verification, Berlin, Germany, July 3-7, 2007
Année
2007
Publisher:
Springer
Mots-clefs:
Laboratoires:




 Notice créée le 2007-05-01, modifiée le 2019-12-05


Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)