SymDiff: Static semantic diff

SymDiff (aka Symbolic Differencing) is an infrastructure for leveraging and extending program verification to reason about program changes (differential program analysis). There are several opportunities for differential program analysis, including (a) performing incremental analysis, (b) use previous versions as a spec to provide relative correctness, and (c) exploit structural similarity to use more scalable and automated 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