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 tool for C programs, that is available internally in MS. We will shortly release an external version soon. Stay tuned!
Visitor
Interns
- 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 and relative termination, no. MSR-TR-2011-112, October 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
