---

Abstract

After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. This paper studies four such approaches in theory and in practice. We compare the following different "schools of thought" of software verification: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification, and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in a unifying theoretical framework, and implement them in the verification framework CPAchecker. Thus, we can present an evaluation that compares the different approaches where the core differences are expressed in configuration parameters, and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches 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
• Version 1.6.18-jar17 of CPAchecker
• 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.