We present a new algorithm for the construction of a correlating program from the syntactic difference between the original and modified versions of a program. This correlating program exhibits the semantics of the two input programs and can then be used to compute their semantic differences, following an approach of Partush and Yahav. We show that Partush and Yahav's correlating program is unsound on loops that include an early exit. Our algorithm is defined on an imperative language with while-loops, break, and continue. To guarantee its correctness, it is formalized and mechanically checked within the Coq proof assistant. On a series of examples, we experimentally find that the static analyzer dizy is at least as precise on our correlating program as on Partush and Yahav's.
展开▼
