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.
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.
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:
For our experiments, we used machines with the following characteristics:
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:
svn checkout https://svn.sosy-lab.org/software/cpachecker/trunk@32864 CPAchecker
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.