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 Citations (Scopus)

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 - 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

Formal methods
Semantics

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, .

Do you trust your compiler? Applying formal methods to constructing high-assurance compilers. / Boyle, James M.; Resler, R. Daniel; Winter, Victor L.

1997. 14-24 Paper presented at Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE, Washington, DC, USA, .

Research output: Contribution to conferencePaper

Boyle, JM, Resler, RD & Winter, VL 1997, 'Do you trust your compiler? Applying formal methods to constructing high-assurance compilers' Paper presented at Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE, Washington, DC, USA, 8/11/97 - 8/12/97, pp. 14-24.
Boyle JM, Resler RD, Winter VL. Do you trust your compiler? Applying formal methods to constructing high-assurance compilers. 1997. Paper presented at Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE, Washington, DC, USA, .
Boyle, James M. ; Resler, R. Daniel ; Winter, Victor L. / Do you trust your compiler? Applying formal methods to constructing high-assurance compilers. Paper presented at Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE, Washington, DC, USA, .11 p.
@conference{c189c1d36bc7434fa73d431068ba1dcc,
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 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.",
author = "Boyle, {James M.} and Resler, {R. Daniel} and Winter, {Victor L.}",
year = "1997",
month = "1",
day = "1",
language = "English (US)",
pages = "14--24",
note = "Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE ; Conference date: 11-08-1997 Through 12-08-1997",

}

TY - CONF

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

AU - Boyle, James M.

AU - Resler, R. Daniel

AU - Winter, Victor L.

PY - 1997/1/1

Y1 - 1997/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0030640719&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0030640719&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:0030640719

SP - 14

EP - 24

ER -