SymDiff: Differential Program Verifier

Established: October 14, 2010

SymDiff is a tool for performing differential program verification. Differential program verification concerns with specifying and proving interesting properties over program differences, as opposed to the program itself. Such properties include program equivalence, but can also capture more general differential/relational properties. SymDiff provides a specification language to state such differential (two-program) properties using the concept of mutual summaries that can relate procedures from two versions. It also provides proof system for checking such differential specifications along with the capability of generating simple differential invariants.

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 (opens in new tab).

The source code of SymDiff (opens in new tab) is on GitHub. This part deals purely with Boogie programs.

Overview

The following tutorial slides provides an overview of SymDiff, as of April 2016:

People

Portrait of Shuvendu Lahiri

Shuvendu Lahiri

Senior Principal Researcher

Portrait of Chris Hawblitzel

Chris Hawblitzel

Senior Researcher