Mutual Summaries: Unifying Program Comparison Techniques

In this paper, we formalize mutual summaries as a contract mechanism for comparing two programs, and provide a method for checking such contracts modularly. We show that mutual summary checking generalizes equivalence checking, conditional equivalence checking and translation validation. More interestingly, it enables comparing programs where the changes are interprocedural. We have prototyped the ideas in SymDiff, a BOOGIE based language-independent infrastructure for comparing programs.