SymDiff (aka Symbolic Differencing) is an infrastructure for leveraging and extending program verification to reason about program changes (differential program analysis). There are several opportunities for differential program analysis, including (a) performing incremental analysis, (b) use previous versions as a spec to provide relative correctness, and (c) exploit structural similarity to use more scalable and automated 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.
Here is an talk that presents an overview of the project.
- 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
- 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
- Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012