Name
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 flow (including loops) in this framework. We demonstrate the usefulness and limitations of the framework for verifying equivalence, compiler optimizations, and interprocedural transformations. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-38574-2_20 | CADE |
Keywords | Field | DocType |
verifying equivalence,unstructured control flow,compiler optimizations,automated theorem provers,general framework,interprocedural transformation,relative termination,single-program verifiers,mutual summary | Programming language,Computer science,Control flow,Correctness,Algorithm,Theoretical computer science,Optimizing compiler,Equivalence (measure theory),Automated theorem provers | Conference |
Citations | PageRank | References |
24 | 0.73 | 10 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chris Hawblitzel | 1 | 578 | 35.08 |
| Ming Kawaguchi | 2 | 155 | 5.19 |
| Shuvendu K. Lahiri | 3 | 1424 | 68.18 |
| Henrique Rebêlo | 4 | 155 | 10.35 |