SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms

Dirk Beyer

and

Matthias Dangl

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:


Results

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

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