Algorithms for Software Model Checking:
Predicate Abstraction vs. Impact

Dirk Beyer and Philipp Wendler

Abstract

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).

Content

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).

• *.xml

  The input files for our benchmarking script.

The rest of the files are from CPAchecker, revision 6013 (branch “forced-covering”).

Results

The result tables of the figures in the paper are available here:

• Table for figure 1 (Impact)
• Table for figure 2 (SBE configurations)
• Table for figure 3 (large-block configurations)

You can click on the cells in the status columns in these tables to see the output of CPAchecker. Clicking on the column headings (e.g., “cputime”) will produce a plot with the quantile function of the values of this column (this requires JavaScript to be enabled).

How to reproduce the results

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.

How to run CPAchecker on a single program

1. Choose one of the configuration files from the "config" directory listed above.
2. Choose one of the benchmark programs in the "programs" directory.
3. Run

   scripts/cpa.sh -heap HEAP_SIZE -config CONFIG_FILE PROGRAM.c

   Example:

   scripts/cpa.sh -heap 2000m -config config/predicate-abstraction-loops.properties test/programs/benchmarks/ntdrivers-simplified/cdaudio_simpl1.cil.c

   Output files of CPAchecker are written to the "output" directory.

How to run CPAchecker on a set of programs

1. Choose a set of configurations (either Impact (Original), Impact (Framework), or Predicate Abstraction).
2. The Java heap size limit is defined in the benchmark definition XML files (“*.xml”). If you have less than 16GB of RAM, you need to adjust this number by changing the following line in the file:

   <option name="-heap">12000m</option>

3. Run the benchmark script

   scripts/benchmark.py

   for the chosen set.
   Example:

   scripts/benchmark.py impact-framework.xml

4. The results (log files and data) will be placed in the “results” directory.