BDD-Based Software Model Checking
with CPAchecker

Dirk Beyer and Andreas Stahlbauer

Abstract

In symbolic software model checking, most approaches use predicates as symbolic representation of the state space, and SMT solvers for computations on the state space; BDDs are sometimes used as auxiliary data structure. The representation of software state spaces by BDDs was not yet thoroughly investigated, although BDDs are successful in hardware verification. The reason for this is that BDDs do not efficiently support all operations that are needed in software verification.

In this work, we evaluate the use of a pure BDD representation of integer variable values, and focus on a particular class of programs: event-condition-action systems with limited operations. A symbolic representation using BDDs seems appropriate for this particular class of programs. We implement a program analysis based on BDDs and experimentally compare three symbolic techniques to verify reachability properties of ECA programs. The results show that BDDs are efficient, which yields the insight that BDDs could be used selectively for some variables (to be determined by a pre-analysis), even in general software model checking.

Please refer to the extended version of this paper.

Supplementary Data

The supplementary archive contains all data, tables, used benchmark programs, and configurations as well as a ready-to-run version of CPAchecker. The archive was built from the branch “trunk” with revision 6607 of the CPAchecker repository. The following files are in this archive:

config/ The CPAchecker configuration files that we used in the experiments.
test/programs/eca/ The benchmark programs.
our-results/ Our raw results, including log files and tables (see also below).
*.xml The input files for our benchmarking script.

Raw Results

The raw result tables are available here: Table for ECA programs. You can click on the cells in the status columns in these tables to see the CPAchecker log file. Clicking on the column headings (e.g., “cputime”) will produce a graph (this requires JavaScript to be enabled).

The corresponding CSV files can be found in the our-results directory.

Reproducing the Results

In order to reproduce the results, download the archive with everything necessary and follow these steps. As the SMT solver used by CPAchecker (MathSAT4) is only available on Linux, this is not possible 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. For the results in the paper, a value of “13000m” was used. You need a machine with at least 16 GB of RAM.

How to run CPAchecker on a single program

  1. Choose one of the configuration files from the config/ directory listed above (e.g., fsmBddAnalysis.properties).
  2. Choose one of the benchmark programs in the test/programs/eca/ directory (e.g., Problem3_25_safe.c).
  3. Run 
    scripts/cpa.sh -heap HEAP_SIZE -config CONFIG_FILE PROGRAM.c
    Example: 
    scripts/cpa.sh -heap 13000m -config config/fsmBddAnalysis.properties test/programs/eca/Problem3_25_safe.c
    ATTENTION: You have to add the parameter -setprop specification=config/specification/default.spc when using the CPAchecker version from the repository!

    Output files of CPAchecker are written to the output directory.

How to run CPAchecker on a set of programs

CPAchecker can be executed with different configurations on a set of programs by using the benchmarking script (scripts/benchmark.py). You can find the input file (eca-bench.xml) for the benchmarking script in the root folder of the supplementary archive.

  1. The Java heap size limit is defined in the benchmark definition XML files. If you have less than 16GB of RAM (or if not enouh memory is free on your machine), you need to adjust this number by changing the following line in the file: 
    <option name="-heap">13000m</option>
  2. Run the benchmark script scripts/benchmark.py with the benchmark definition file. Example: 
    scripts/benchmark.py eca-bench.xml
  3. The results (log files and data) will be placed in the directory test/results/.