A Unifying View on SMT-based Software Verification

Dirk Beyer, Matthias Dangl, and Philipp Wendler

A preprint of this article is available for you to download.


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:


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.