Augmenting Predicate Analysis
with Auxiliary Invariants

Master's Thesis in Computer Science at the Chair for Software Systems at the University of Passau
— Supplementary Web Page —
Thesis
Presentation

Thomas Stieglmaier

Abstract

Predicate analysis is a common approach to software model checking. Abstractions of programs are computed out of predicates found with craig interpolation. The found interpolants are, however, in some cases not ideal, and lead to long-running verification runs. To reduce the reliance on interpolation this thesis evaluates the effects of using separately computed, auxiliary, invariants instead.

Our work is based on the CPA concept, CPAchecker and the PredicateCPA. It is split into two major parts, on the one hand we introduce a new algorithm for concurrent execution of several analysis in CPAchecker, as well as communication between such analysis, and on the other hand we show how the PredicateCPA can be augmented with additional formulas in several ways, we chose to evaluate: appending invariants to the precision of the analysis and conjoining invariants either to the path formula or to the abstraction formula. The invariants we want to use are generated by some new approaches directly in CPAchecker. They can be separated in two classes, on the one hand the on-the-fly and lightweight invariant generation heuristics which try to find invariants for a certain given program location only, and on the other hand complete analyses, which results are then used for generating invariants for the whole program.

While the lightweight on-the-fly approaches did not yield the expected results, analyses using concurrently computed invariants perform strictly better than comparable analyses without invariants.

Complete Results

The complete results from our experiments, can be found in the tables listed below.

Wrong Invariant

In the following paragraph we see a path formula and an invariant for the program heap-manipulation/sll_to_dll_rev_false-unreach-call.i where the conjunction of the invariant and the path formula leads to a wrong proof. This is caused by different handling of pointer variables in the Predicate CPA and the Invariants CPA.

The resulting formula of conjoining this path formula with this invariant is unsatisatisfiable, leading to a wrong result with the predicate analysis. The interpolant between these formulas is showing the problem: (assert (not (= |main::list@3| (_ bv0 32)))) tells us that the variable |main::list@3| has the value 0. However, this variable is a pointer and the Predicate CPA handles pointers with uninterpreted functions and does not expect that a pointer is 0. The different values for this variable lead to the unsatisfiability.

The following commandline can be used to observe this behavior:

scripts/cpa.sh
-noout
-heap 6000M
-setprop solver.solver=MATHSAT5
-setprop cpa.predicate.refinement.performInitialStaticRefinement=false
-setprop cpa.predicate.ignoreIrrelevantFields=false
-setprop cpa.predicate.ignoreIrrelevantVariables=false
-pred-Invgen-parallel-bitprecise
-setprop cpa.predicate.invariants.appendToPathFormula=true
-setprop cpa.predicate.invariants.appendToAbstractionFormula=true
-timelimit 600s
-stats
-spec test/programs/benchmarks/heap-manipulation/ALL.prp
test/programs/benchmarks/heap-manipulation/sll_to_dll_rev_false-unreach-call.i

Benchmarking Configurations

In order to allow reproducibility of the evaluation, this section briefly describes how the necessary CPAchecker revisions can be obtained and which configurations were used.

CPAchecker needs to be available in revision 23084 (trunk), for the path invariants benchmarks either in revision 23143 (trunk) or better 23146 (branches/pathInvariants-fix). Furthermore some benchmarks with Z3 as solver were done on revision 23206 after the main evaluation was finished. Additionally we need the benchmarks from the SV-Comp. They are available in the c folder of the SV-Comp GitHub repository.

  1. Change into the CPAchecker directory
  2. Download all dependencies and build CPAchecker by executing ant
  3. Run the shell script scripts/benchmark.py, for example, by using the command below:
    scripts/benchmark.py path/to/predicate_bitprecise_parallel.xml
  4. The command above expects the correct path to your benchmark configuration file. Please note that you might have to adjust the paths in the benchmark set files referenced in the used benchmark configuration. For comparable results the used CPU should be the same as the one used in our experiments.
  5. The results (log files and data) will be placed in the directory test/results/.

All benchmark configurations are listed here:

All benchmark sets are listed here: