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 conferencePaper

3 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
Publication statusPublished - Jan 1 1997
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

    Fingerprint

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Boyle, J. M., Resler, R. D., & Winter, V. L. (1997). Do you trust your compiler? Applying formal methods to constructing high-assurance compilers. 14-24. Paper presented at Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE, Washington, DC, USA, .