Mutual Summaries: Unifying Program Comparison Techniques
- Chris Hawblitzel ,
- Ming Kawaguchi ,
- Shuvendu Lahiri ,
- Henrique Rebelo
MSR-TR-2011-78 |
Informal proceedings of BOOGIE 2011 workshop
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.