Explicit-Value Analysis Based on CEGAR and Interpolation

Dirk Beyer and Stefan Löwe

This work was presented at FASE 2013 and won the ETAPS Test-of-Time Award.
The published article is available open access for you to download, published in Proc. FASE 2013.

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:

```
table-cpa_expl.html/table-cpa_expl.csv
```
the table comparing CPA-EXPL and CPA-EXPLitp, both as HTML as well as CSV file
```
table-cpa_expl_pred.html/table-cpa_expl_pred.csv
```
the table comparing CPA-PRED, CPA-EXPLitp, CPA-EXPL-PRED and CPA-EXPLitp-PRED, both as HTML as well as CSV file
```
*.logfiles/
```
folders that contain the very detailed logfiles of each verification run. The command line for starting CPAchecker with the respective configuration and benchmark file can be found in the very first line of the respective logfile

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

svn co -r 6615 https://svn.sosy-lab.org/software/cpachecker/trunk explicitCegar

```
cd explicitCegar
```
```
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:

the configurations that utilize a predicate analysis will only run under Linux, as this depends on MathSAT4, which does not work on the Windows platform
you may have to alter the -heap command line arguement to fit your environment. 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 “12500m” was used.

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.