Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report)

TL;DR

This paper enhances difference verification with conditions by introducing a more precise difference detector that considers data dependencies and program properties, leading to improved effectiveness and efficiency.

Contribution

It proposes diffDP, a new difference detector that improves over syntax-based methods by incorporating data dependencies and properties for better overapproximation.

Findings

diffDP improves verification accuracy

Enhanced efficiency in difference verification tasks

More effective detection of potential property violations

Abstract

Software changes frequently. To efficiently deal with such frequent changes, software verification tools must be incremental. Most of today's approaches for incremental verification consider one specific verification approach. One exception is difference verification with conditions recently proposed by Beyer et al. Its underlying idea is to determine an overapproximation of those modified execution paths that may cause a new property violation, which does not exist in the unchanged program, encode the determined paths into a condition, and use the condition to restrict the verification to the analysis of those determined paths. To determine the overapproximation, Beyer et al. propose a syntax-based difference detector that adds any syntactical path of the modified program that does not exist in the original program into the overapproximation. This paper provides a second difference detector diffDP, which computes a more precise overapproximation by taking data dependencies and program properties into account when determining the overapproximation of those modified execution paths that may cause a new property violation. Our evaluation indeed shows that our more precise difference detector improves the effectiveness and efficiency of difference verification with condition on several tasks.