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
- (short and more up to date) Presentation at Program Equivalence Workshop, April 2016 at London, UK.
- (longer) Tutorial slides (Halmstad Summer School on Testing, 2015) provides an overview of SymDiff, as of June 2015.
- Shuvendu Lahiri, Rohit Sinha, and Chris Hawblitzel, Automatic Rootcausing for Program Equivalence Failures in Binaries, in Computer Aided Verification (CAV'15), Springer, July 2015.
- Shaobo He, Shuvendu K. Lahiri, and Zvonimir Rakamaric, Verifying Relative Safety, Accuracy, and Termination for Program Approximations, April 2016.
- Shuvendu Lahiri, Rohit Sinha, and Chris Hawblitzel, Automatic Rootcausing for Program Equivalence Failures in Binaries, no. MSR-TR-2014-11, February 2014.
- Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, and Scott Wadsworth, Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation, in Foundations of Software Engineering (FSE'13), ACM, August 2013.
- Shuvendu Lahiri, Ken McMillan, Rahul Sharma, and Chris Hawblitzel, Differential Assertion Checking, in Foundations of Software Engineering (FSE'13), ACM, August 2013.
- 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 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.
- Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo, Mutual Summaries: Unifying Program Comparison Techniques, no. MSR-TR-2011-78, 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.
- Francesco Logozzo, Shuvendu Lahiri, Manuel Fahndrich, and Sam Blackshear, Verification Modulo Versions: Towards Usable Verification, in Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014), ACM SIGPLAN, June 2014.
- 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.