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.
- Shuvendu Lahiri, Rohit Sinha, and Chris Hawblitzel, Automatic Rootcausing for Program Equivalence Failures in Binaries, in Computer Aided Verification (CAV'15), Springer, July 2015.
- Shuvendu K. Lahiri, Arvind Haran, Shaobo He, and Zvonimir Rakamaric, Automated Differential Program Verification for Approximate Computing, May 2015.
- 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.