Augmenting Predicate Analysis with Auxiliary InvariantsMaster's Thesis in Computer Science at the Chair for Software Systems at the University of Passau
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.
The complete results from our experiments, can be found in the tables listed below.
- Results for (lightweight) heuristics
- Results for sequential analyses
- Results for parallel analyses
- Results for lightweight heuristics with Z3 as SMT solver
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.
(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:
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
of the SV-Comp GitHub repository.
- Change into the CPAchecker directory
- Download all dependencies and build CPAchecker by executing
Run the shell script
scripts/benchmark.py, for example, by using the command below:
- 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.
- The results (log files and data) will be placed in the directory
All benchmark configurations are listed here:
- Baseline 300s
- Baseline 600s
- Baseline, Portofolio of Predicate Analysis and Invariant Generation
- Inductive Weakening of Path Formulas
- Inductive Weakening of Path Formulas
- Checking Interpolants on Invariance (Abstraction at Loop Heads)
- Checking Interpolants on Invariance (Abstraction at Loop Heads and Join Points)
- Path Invariants
- Parallel Combinations ofAnalyses
- Sequential Combinations of Analyses