zbMATH — the first resource for mathematics

Configurable software verification: Concretizing the convergence of model checking and program analysis. (English) Zbl 1135.68466
Damm, Werner (ed.) et al., Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73367-6/pbk). Lecture Notes in Computer Science 4590, 504-518 (2007).
Summary: 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.
For the entire collection see [Zbl 1119.68005].

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI