SymDiff is an infrastructure for leveraging and extending program verification to reason about relationship between two programs (differential program analysis). There are several opportunities for differential analysis, including (a) performing incremental analysis, (b) use one program as a spec to provide relative correctness, (c) check differential properties (such as equivalence) and (d) exploit structural similarity to use more scalable abstractions.
The tool is language-independent and works at the level of Boogie programming language. The intent is to be able to target various source languages (C, C++, .NET, x86) using translators to Boogie. We currently have a front end for C and Boogie programs for download.
The source code of SymDiff is on Codeplex. This part deals purely with Boogie programs.
The following tutorial slides provides an overview of SymDiff, as of June 2015: