Do you trust your compiler? Applying formal methods to constructing high-assurance compilers

James M. Boyle, R. Daniel Resler, Victor L. Winter

Research output: Contribution to conferencePaperpeer-review

4 Scopus citations

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 some 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 from the correctness of the transformations.

Original languageEnglish (US)
Pages14-24
Number of pages11
StatePublished - 1997
Externally publishedYes
EventProceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE - Washington, DC, USA
Duration: Aug 11 1997Aug 12 1997

Other

OtherProceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE
CityWashington, DC, USA
Period8/11/978/12/97

ASJC Scopus subject areas

  • General Engineering

Fingerprint

Dive into the research topics of 'Do you trust your compiler? Applying formal methods to constructing high-assurance compilers'. Together they form a unique fingerprint.

Cite this