Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
SymDiff: Differential program verifier

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.

We have also released the source code of SymDiff on Codeplex. This part deals purely with Boogie programs.

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



Other publications about differential program analysis