Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo
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.
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo. Towards Modularly Comparing Programs using Automated Theorem Provers, October 2011.