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, or about program differences (hence 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 slides provide a quick introduction to SymDiff

  1. (short and more up to date) Presentation at Program Equivalence Workshop, April 2016 at London, UK.
  2. (longer) Tutorial slides (Halmstad Summer School on Testing, 2015) provides an overview of SymDiff, as of June 2015.



Other publications about differential program analysis