SymDiff: Differential program verifier

SymDiff (aka Symbolic Differencing) 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 previous versions 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.

Here is an talk that presents an overview of the project.



Other publications about differential program analysis