Explicit-Value Analysis Based on CEGAR and Interpolation

Dirk Beyer and Stefan Löwe


Abstract

Abstraction, counterexample-guided abstraction refinement, and interpolation are essential techniques for software model checking. However, while these techniques are successfully used in symbolic approaches, they are almost unused in explicit-value model checking. We develop an approach and tool implementation that integrate abstraction and interpolation-based refinement into an explicit-value analysis — an analysis that tracks for a specified set of variables their explicit values. The algorithm uses an ART as central data structure and an path-sensitive dynamic approach for precision adjustment. We evaluate our algorithm on the benchmark set of the 2012 Competition on Software Verification (SV-COMP’12), and show that our new approach is highly competitive, and when combined with an auxiliary predicate analysis, even scores higher than the SV-COMP’12 winner.


Content

The supplementary archive contains all data from our experiments. The following files are in this archive:

For obtaining CPAchecker, we refer to our public repository. To install CPAchecker, run the following commands:

  1. svn co -r 6615 https://svn.sosy-lab.org/software/cpachecker/trunk explicitCegar
  2. cd explicitCegar
  3. ant

To then run a benchmark with, e.g., our first configuration, run:

scripts/cpa.sh -heap 12500M -noout -explicitAnalysis -stats test/programs/benchmarks/ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c

Note:


Results

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

You can click on the cells in the status columns in these tables to see the output of CPAchecker.