Difference Verification with Conditions

— Supplemental Material —

Dirk Beyer, Marie-Christine Jakobs and Thomas Lemberger

Abstract

Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques, and most of them must be integrated in the development process before the software system grows too large to be analyzed as a whole.
To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software have changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes.
As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions to make three existing verifiers capable of incremental verification. An extensive evaluation shows the competitiveness of difference verification with conditions.

Supplementary Data for Experiments

We performed an extensive experimental evaluation to show the feasibility ofdifference verification with conditions. In the following, we provide our experimental (raw) data, detailed information on the experimental setup including references to the tools and tasks used, as well as a description how to repeat our experiments.

Experimental Results

A table listing all experimental results can be found here (CSV).

The raw data of our experiments can be found here.

For the two verifiers, which are no conditional verifiers, namely CPA-seq and UAutomizer, we used the reducer-based approach to enable difference verification with conditions. This is reflected in our experiments. For these two verifiers, we split difference verification with conditions into two parts: (1) algorithm diffCond plus reducer and (2) verification of the residual program. Both parts are executed in different runs. Since the first part is the same for both verifiers, we only executed it once. The residual programs generated by the first part can be downloaded here:

To apply precision reuse, we need the initial precisions, which we constructed during a verification of the original program. The set of initial precisions is available for download, too.

Experimental Setup

Computing Environment

For our experiments, we used machines with the following characteristics:


The granted resources for each analysis run, which we enforced with the tool BenchExec, version 2.3, were

Tools

To experiment with difference verification with conditions, we need (1) an implementation of the diffCond algorithm and (2) (conditional) verifiers. We used the conditional verifier predicate analysis, which is implemented in CPAchecker, and turned the verifiers CPA-seq (part of CPAchecker) and UAutomizer into conditional verifiers using the reducer-based approach with the ParComp reducer implemented in CPAchecker. Additionally, we compared and combined difference verification with an orthogonal incremental verification approach named precision reuse, which is also integrated into CPAchecker the for predicate analysis. Hence, we used the following tools to perform our experiments:

Tasks and Benchmark Definitions

In our experiments, we used the following tasks and benchmark definitions:

Repeating our Experiments and Usage

We provide a replication artifact and a repository that contains all material necessary to repeat our experiments and recreate the tables and plots presented in our submission. Both artifact and repository also contain a tutorial on the usage of difference verification with conditions.