Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Towards Modularly Comparing Programs using Automated Theorem Provers

Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo

Abstract

In this paper, we present a general framework for modularly comparing two (imperative) programs that can leverage single-program verifiers based on automated theorem provers. We formalize (i) mutual summaries for comparing the summaries of two programs, and (ii) relative termination to describe conditions under which two programs relatively terminate. The two rules together allow for checking correctness of interprocedural transformations. We also provide a general framework for dealing with unstructured control fow (including loops) in this framework. We demonstrate the usefulness and limitations of the framework for verifying equivalence, compiler optimizations, and interprocedural transformations.

Details

Publication typeTechReport
NumberMSR-TR-2011-112

Previous versions

Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo. Mutual Summaries: Unifying Program Comparison Techniques, August 2011.

> Publications > Towards Modularly Comparing Programs using Automated Theorem Provers