---

Abstract

After many years of successful development of new algorithms for software model checking, there is a need to consolidate the knowledge about the different algorithms and approaches. This paper gives a coarse overview in terms of effectiveness and efficiency of four algorithms. We compare the following different "schools of thought" of algorithms: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those algorithms are well-known and successful in software verification. They have in common that they are based on SMT solving as the back-end technology, using the theories of uninterpreted functions, bit vectors, and floats as underlying theory. All four algorithms are implemented in the verification framework CPAchecker. Thus, we can present an evaluation that really compares only the core algorithms, and keeps the design variables such as parser front end, SMT solver, used theory in SMT formulas, etc. constant. We evaluate the algorithms on a large set of verification tasks, and discuss the conclusions.

---

Content

The supplementary archive contains CPAchecker and all data from our experiments. The following files are in this archive:

• The additional test-set definitions used for the experiments
• CPAchecker in version cpachecker-1.6.8-vstte
• The results presented in our paper
• A README file explaining how to reproduce the results

---

Results

The result tables of the figures in our article are also available:

• Table for all algorithms on all categories
• Table of differences between all algorithms on all categories
• Table for all algorithms on all category of Linux device drivers (DeviceDriversLinux64)
• Table of differences between all algorithms on the category of Linux device drivers (DeviceDriversLinux64)
• Table for all algorithms on the category of event condition action systems (ECA)
• Table of differences between all algorithms on the category of event condition action systems (ECA)
• Table for all algorithms on the category of product lines (ProductLines)
• Table of differences between all algorithms on the category of product lines (ProductLines)

You can click on the cells in the status columns of the different algorithms in these tables to see their log output.