Abstract

Verification is a complex algorithmic task, requiring large amounts of computing resources. One approach to reduce the resource consumption is to reuse information from previous verification runs. This paper gives an overview of three techniques for such information reuse. Conditional model checking outputs a condition that describes the state space that was successfully verified, and accepts as input a condition that instructs the model checker which parts of the system should be verified; thus, later verification runs can use the output condition of previous runs in order to not verify again parts of the state space that were already verified. Precision reuse is a technique to use intermediate results from previous verification runs to accelerate further verification runs of the system; information about the level of abstraction in the abstract model can be reused in later verification runs. Typical model checkers provide an error path through the system as witness for having proved that a system violates a property, and a few model checkers provide some kind of proof certificate as a witness for the correctness of the system; these witnesses should be such that the verifiers can read them and —with less computational effort— (re-) verify that the witness is valid.

Examples

We show an example for a counterexample automaton that can be used to guide a verifier along a specific (error) path through a program in order to re-verify a counterexample (c.f. Section 4 and Figure 4 of the paper).

Supplementary Data

The supplementary archive contains all data, tables, used benchmark programs, and configurations as well as a ready-to-run version of CPAchecker. The archive was built from the branch “trunk” with revision 7952 of the CPAchecker repository. The following (relevant) files are in this archive:

config/	The CPAchecker configuration files that we used in the experiments.
programs/	The analyzed programs.
our-results/	Our raw results, including log files and tables (see also below).
*.xml	The input files for our benchmarking script: reusingverificationresults-precision-safe.xml: Precision reuse for safe programs. reusingverificationresults-precision-unsafe.xml: Precision reuse for unsafe programs. reusingverificationresults-errorpaths.xml: Re-verification of counterexamples.

Full Results for Conditional Model Checking

The full results are available in the paper “Conditional Model Checking: A Technique to Pass Information between Verifiers” and the respective supplementary webpage.

Full Results for Precision Reuse

The full result tables are available here:

• Raw results for explicit analysis (safe programs)
• Raw results for predicate analysis (safe programs)
• Raw results for explicit analysis (unsafe programs)
• Raw results for predicate analysis (unsafe programs)

The first columns show the results of the initial run (without reuse), the remaining columns show the results of the run that reuses precisions. You can click on the cells in the status columns in these tables to see the CPAchecker log file. Clicking on the column headings (e.g., “cputime”) will produce a graph (this requires JavaScript to be enabled).

The corresponding CSV files can be found in the our-results directory of the supplementary archive.

Full Results for Re-verification of Counterexamples

The full result tables are available here:

• Raw results for explicit analysis
• Raw results for predicate analysis

The first columns show the results of the initial run, the remaining columns show the results of the re-verification runs. You can click on the cells in the status columns in these tables to see the CPAchecker log file. Clicking on the column headings (e.g., “cputime”) will produce a graph (this requires JavaScript to be enabled).

The corresponding CSV files can be found in the our-results directory of the supplementary archive.

Reproducing the Results

In order to reproduce the results, download the supplementary archive and follow these steps. Linux is required to run the experiments because the SMT solver used by CPAchecker (MathSAT5) is only available for Linux.

CPAchecker requires that the amount of memory used for the Java heap is set according to the memory of your machine. If this parameter is higher than the available memory, the JVM will not start. For the results in the paper, a value of “14000m” was used; the whole process (including the RAM that was used by the SMT solver) was limited to 15 GB of RAM.

The benchmark script uses the “control groups” feature of the Linux kernel for reliable time and memory measurements. On most system, this feature needs to be enabled first, and the current user needs to be given permission to use it. This can be achieved with the following two commands:

sudo mount -t cgroup none /sys/fs/cgroup
sudo chmod o+wt /sys/fs/cgroup