SymDiff (aka Symbolic Differencing) is an infrastructure for leveraging and extending program verification to reason about program changes. In a nutshell, Symdiff can be summarized as Windiff for behaviors. It builds up on recent advances on program equivalence checking using automated SMT solvers. However, it extends beyond program equivalence and deals with questions such as: (1) can one infer the conditions under which two programs are equivalent? (2) how do the changes affect the public API?
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.
- Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebelo, Towards Modularly Comparing Programs using Automated Theorem Provers, in International Conference on Automated Deduction (CADE '13), Springer, June 2013
- Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris Hawblitzel, Differential Assertion Checking, no. MSR-TR-2013-34, March 2013
- Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Rebelo, SymDiff: A language-agnostic semantic diff tool for imperative programs, in Computer Aided Verification (CAV '12) (Tool description), Springer, July 2012
- Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012
- Patrice Godefroid, Shuvendu Lahiri, and Cindy Rubio-González, Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation, in Static Analysis Symposium (SAS '11), Lecture Notes in Computer Science, August 2011
- Shuvendu K. Lahiri, Kapil Vaswani, and Tony Hoare, Differential Static Analysis: Opportunities, Applications, and Challenges, in 2010 FSE/SDP Workshop on the Future of Software Engineering Research (Position paper) , Association for Computing Machinery, Inc., November 2010
- Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebelo, Conditional equivalence, no. MSR-TR-2010-119, October 2010