Dirk Beyer and Philipp Wendler
CEGAR, SMT solving, and Craig interpolation are successful approaches for software model checking. We compare two of the most important algorithms that are based on these techniques: lazy predicate abstraction (as in BLAST) and lazy abstraction with interpolants (as in IMPACT). We unify the algorithms formally (by expressing both in the CPA framework) as well as in practice (by implementing them in the same tool). This allows us to flexibly experiment with new configurations and gain new insights, both about their most important differences and commonalities, as well as about their performance characteristics. We show that the essential contribution of the IMPACT algorithm is the reduction of the number of refinements, and compare this to another approach for reducing refinement effort: adjustable-block encoding (ABE).
The supplementary archive contains all data, tables, used benchmark programs, and configurations as well as a ready-to-run version of CPAchecker. The following files are in this archive:
config/The CPAchecker configuration files that we used in the experiments.
test/programs/The benchmark programs.
our-results/Our raw results, including log files and tables (see also below).
*.xmlThe input files for our benchmarking script.
The rest of the files are from CPAchecker, revision 6013 (branch “forced-covering”).
The result tables of the figures in the paper are available here:
In order to reproduce the results, download the archive with everything necessary and follow the following steps. The SMT solver that CPAchecker uses (MathSAT4) is only available for GNU/Linux, thus, the experiments cannot be repeated on other platforms.
CPAchecker requires that the amount of memory used for the Java heap is set according to the memory of your machine. If this parameter is higher than the available memory, the JVM will not start. A good start is a value of “2000m” if you have at least 3-4GB of RAM. For the results in the paper, a value of “12000m” was used.
scripts/cpa.sh -heap HEAP_SIZE -config CONFIG_FILE PROGRAM.cExample:
scripts/cpa.sh -heap 2000m -config config/predicate-abstraction-loops.properties test/programs/benchmarks/ntdrivers-simplified/cdaudio_simpl1.cil.cOutput files of CPAchecker are written to the "output" directory.
scripts/benchmark.pyfor the chosen set.