Effective Approaches
to Abstraction Refinement
for Automatic Software Verification

— Supplementary Web Page —
Thesis     Presentation

Stefan Löwe

Plain Value Analysis

In order to allow reproducibility of the evaluation, this section briefly describes the configuration and holds the detailed results of the plain value analysis, as described in Chapter 3 of the thesis.

The following shows how the plain value analysis was configured for the evaluation performed in the thesis. Running the value analysis with in configuration on a single verification task is shown below.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Plain -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Value Analysis with CEGAR and Interpolation

In order to allow reproducibility of the evaluation, this section briefly describes the configuration and holds the detailed results of the value analysis with CEGAR and interpolation, as described in Chapter 4 of the thesis.

The following shows how the value analysis with CEGAR and interpolation was configured for the evaluation performed in the thesis. Running the value analysis with in configuration on a single verification task is shown below.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

The original supplementary web page for the publication at FASE'13 is available here.

Value Analysis with Heuristics for Optimized Interpolation

In order to allow reproducibility of the evaluation, this section briefly describes the configuration and holds the detailed results of the value analysis with heuristics for optimized interpolation, as described in the first part of Chapter 5 of the thesis.

The following shows how the value analysis with heuristics for optimized interpolation was configured for the evaluation performed in the thesis. Running the value analysis in this configuration on a single verification task is shown below. Note that the example below enables all optimizations by setting cpa.value.interpolation.applyItpEqualityOptimization, cpa.value.interpolation.applyRenamingOptimization, and cpa.value.interpolation.applyUnsatSuffixOptimization to true. To disable any of the optimizations just set the respective option to false.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=true -setprop cpa.value.interpolation.applyRenamingOptimization=true -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=true -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Value Analysis with Improved CEGAR and Interpolation

In order to allow reproducibility of the evaluation, this section briefly describes the configuration and holds the detailed results of the value analysis with improved CEGAR and interpolation, as described in the second part of Chapter 5 of the thesis.

The following shows how the value analysis with improved CEGAR and interpolation was configured for the evaluation performed in the thesis. Running the value analysis in this configuration on a single verification task is shown below.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar-Optimized -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Composite Analysis based on CEGAR

In order to allow reproducibility of the evaluation, this section briefly describes the configuration and holds the detailed results of the composite analysis based on CEGAR, as described in Chapter 6 of the thesis.

The following shows how the composite analysis based on CEGAR was configured for the evaluation performed in the thesis. Running the composite analysis in this configuration on a single verification task is shown below.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar-Optimized -setprop CompositeCPA.cpas=cpa.location.LocationCPA,cpa.callstack.CallstackCPA,cpa.functionpointer.FunctionPointerCPA,cpa.value.ValueAnalysisCPA,cpa.predicate.PredicateCPA -setprop cegar.refiner=cpa.value.refiner.ValueAnalysisDelegatingRefiner -setprop cpa.predicate.blk.alwaysAtJoin=true -setprop cpa.predicate.blk.alwaysAtFunctions=false -setprop cpa.predicate.blk.alwaysAtLoops=true -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Refinements over Infeasible Sliced Prefixes

In order to allow reproducibility of the evaluation, this section briefly describes the configurations and holds the detailed results of applying refinements over infeasible sliced prefixes for the value analysis, as well as for the predicate analysis with different block-encoding strategies, as described throughout Chapter 7 of the thesis.

Refinements over Infeasible Sliced Prefixes for the Value Analysis

The following shows how the value analysis was configured for the evaluation performed in the thesis. Running the value analysis in the respective configuration on a single verification task is shown below. Note that in the example, by setting the option cpa.value.refinement.prefixPreference to LENGTH_MIN the analysis is configured to prefer the refinement with the shortest infeasible prefix. Other values for the option used in this evaluation are LENGTH_MAX, LENGTH_RANDOM and LENGTH_NONE, the latter disabling the application of refinements over infeasible sliced prefixes.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar-Optimized -setprop cpa.value.refinement.prefixPreference=LENGTH_MIN -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Refinements over Infeasible Sliced Prefixes for the Predicate Analysis (SBE)

The following shows how the predicate analysis, with SBE as block-encoding strategy, was configured for the evaluation performed in the thesis. Running the predicate analysis in the respective configuration on a single verification task is shown below. Note that in the example, by setting the option cpa.predicate.refinement.prefixPreference to LENGTH_MIN the analysis is configured to prefer the refinement with the shortest infeasible prefix. Other values for the option used in this evaluation are LENGTH_MAX, LENGTH_RANDOM and LENGTH_NONE, the latter disabling the application of refinements over infeasible sliced prefixes.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=LENGTH_MIN -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Refinements over Infeasible Sliced Prefixes for the Predicate Analysis (ABE)

The following shows how the predicate analysis, using different large-block-encoding strategies, was configured for the evaluation performed in the thesis. Running the predicate analysis in the respective configuration on a single verification task is shown below. Note that in the example, by setting the option cpa.predicate.refinement.prefixPreference to LENGTH_MAX the analysis is configured to prefer the refinement with the shortest infeasible prefix. The only other value for the option used in this evaluation is LENGTH_NONE, which disables the application of refinements over infeasible sliced prefixes. Furthermore, in the example the block-encoding strategy ABE-l is used. For ABE-lf and ABE-lj the options cpa.predicate.blk.alwaysAtFunctions and cpa.predicate.blk.alwaysAtJoin, respectively, must be set to true.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.blk.alwaysAtLoops=true -setprop cpa.predicate.blk.alwaysAtFunctions=false -setprop cpa.predicate.blk.alwaysAtJoin=false -setprop cpa.predicate.refinement.prefixPreference=LENGTH_MIN -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

The original supplementary web page for the publication at FORTE'15 is available here.

Guided Refinement Selection

In order to allow reproducibility of the evaluation, this section briefly describes the configurations and holds the detailed results of applying guided refinement selection for the value analysis, for the predicate analysis, as well as for a combintation of the value and the predicate analysis, as described in Chapter 8 of the thesis.

Guided Refinement Selection for the Value Analysis

The following shows how the value analysis was configured for the evaluation performed in the thesis. Running the value analysis in the respective configuration on a single verification task is shown below. Note that in the example, by using DOMAIN_MIN as the primary refinement-selection heuristic the analysis is configured to prefer the refinement associated with the lowest domain-type score. Examples for other values in this evaluation are DOMAIN_MAX, WIDTH_MIN, WIDTH_MAX, PIVOT_MIN, PIVOT_MAX, LENGTH_MIN, LENGTH_MAX, RANDOM, or NONE. In case where the selection heuristic might return identical scores for different refinements we add LENGTH_MAX as tie-breaker where needed.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar-Optimized -setprop cpa.value.refinement.prefixPreference=DOMAIN_MIN,LENGTH_MAX -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Guided Refinement Selection for the Predicate Analysis

The following shows how the predicate analysis was configured for the evaluation performed in the thesis. Running the predicate analysis in the respective configuration on a single verification task is shown below. Note that in the example, by using DOMAIN_MIN as the primary refinement-selection heuristic the analysis is configured to prefer the refinement associated with the lowest domain-type score. Examples for other values in this evaluation are DOMAIN_MAX, WIDTH_MIN, WIDTH_MAX, PIVOT_MIN, PIVOT_MAX, LENGTH_MIN, LENGTH_MAX, RANDOM, or NONE. In case where the selection heuristic might return identical scores for different refinements we add LENGTH_MAX as tie-breaker where needed.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=DOMAIN_MIN,LENGTH_MAX -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

Inter-Analysis Refinement Selection

The following shows how the composite analysis of a value and predicate analysis was configured for the evaluation performed in the thesis. Running the composite analysis in the respective configuration on a single verification task is shown below.

CPAchecker needs to be available in revision 20406, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 20406 cpachecker20406

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker20406
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.blk.threshold=1 -setprop cpa.predicate.abstraction.computation=CARTESIAN -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -valueAnalysis-ItpRefiner-ABEl -setprop cpa.predicate.refinement.prefixPreference=DOMAIN_MIN,LENGTH_MAX -setprop cpa.value.refinement.restart=ROOT -setprop cpa.value.refinement.prefixPreference=DOMAIN_MIN,LENGTH_MAX -setprop cegar.useRefinementSelection=true -setprop cegar.domainScoreThreshold=2147483646 -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/byte_add_false-unreach-call.i
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The complete results from our experiments, including all logs, are browsable in an interactive table.

The original supplementary web page for the publication at SPIN'15 is available here.

CPA-RefSel-Plus

In order to allow reproducibility of the evaluation, this section briefly describes the configuration and holds the detailed results of the CPAchecker configuration we refer to as CPA-RefSel-Plus, as described in Chapter 9 of the thesis.

The following shows how CPA-RefSel-Plus was configured for the evaluation performed in the thesis. Running the analysis with in configuration on a single verification task is shown below.

CPAchecker needs to be available in revision 21270, e.g., via executing the following command:

svn co https://svn.sosy-lab.org/software/cpachecker/trunk -r 21270 cpachecker21270

  1. Change into the directory from above, e.g., by executing the following command:
    cd cpachecker21270
  2. Download all dependencies and build CPAchecker by executing the following command:
    ant
  3. Run the shell script scripts/cpa.sh, for example, by using the command below:
    scripts/cpa.sh -valueAnalysis-predicateAnalysis--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -stats -spec test/programs/benchmarks/ntdrivers-simplified/ALL.prp test/programs/benchmarks/ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c
  4. The command above expects the specification file ALL.prp and the benchmark program to be available at the respective paths.
  5. The results (log files and data) will be placed in the directory output/.

The results from our experiments are available in browsable interactive tables.