diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions

To deal with frequent software changes, as e.g., caused by agile software development processes, software verification tools must be incremental. While many existing incremental verification approaches are tailored to and coupled with a specific verifier, Beyer et al. recently introduced a verifier agnostic approach. The underlying idea of their approach is to (1) detect an overapproximation of those paths in the modified software that may cause regression bugs (i.e., property violations that do not exist in the original, unmodified software), (2) encode the detected paths in a condition, and (3) apply conditional model checking to restrict the verifier’s exploration to the detected paths. So far, only a simple, syntax-based difference detector exists. In this paper, we propose a more complicated difference detector diffDP, which amongst others takes data dependencies and correctness properties (more concretely, (un)reachability properties) into account to determine which changes may cause regression bugs where. Our extensive evaluation confirms that for all considered conditional model checkers our proposed difference detector improves the effectiveness and efficiency of difference verification with condition on several tasks.