Name
Title | ||
|---|---|---|
Do You Trust Your Compiler? Applying Formal Methods to Constructing High-Assurance Compilers |
Abstract | ||
|---|---|---|
This paper describes how automatic transformation technology can be used to construct a verified compiler for an imperative language. Our approach is to "transformationally" pass a source program through a series of canonical forms each of which correspond to sonic goal or objective in the compilation process (e.g., introduction of registers, simplification of expressions, etc.).We describe a denotational semantic based framework in which it is possible to verify the correctness of transformations; The correctness of the compiler follows fi om the correctness of the transformations. |
Year | DOI | Venue |
|---|---|---|
1997 | 10.1109/HASE.1997.648033 | HASE |
Keywords | Field | DocType |
constructing high-assurance compilers,formal methods,engines,formal method,canonical forms,computer architecture,reliability engineering,formal verification,denotational semantics,programming language,imperative language,redundancy,canonical form,software reliability,registers,computer bugs,aerospace engineering | Functional compiler,Programming language,Computer science,Compiler correctness,Correctness,Denotational semantics,Compiler,Compiler construction,Formal methods,Formal verification | Conference |
ISBN | Citations | PageRank |
0-8186-7971-9 | 4 | 0.54 |
References | Authors | |
5 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| James M. Boyle | 1 | 587 | 57.16 |
| R. Daniel Resler | 2 | 22 | 3.48 |
| Victor L. Winter | 3 | 110 | 17.04 |