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

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

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

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

Computer Science

Research output: Contribution to conference › Paper

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 language	English (US)
Pages	14-24
Number of pages	11
State	Published - 1997
Event	Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE - Washington, DC, USA Duration: Aug 11 1997 → Aug 12 1997

Other

Other	Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE
City	Washington, DC, USA
Period	8/11/97 → 8/12/97

ASJC Scopus subject areas

Engineering(all)

Access to Document

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

@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",

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

Y1 - 1997

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

T2 - Proceedings of the 1997 High-Assurance Systems Engineering Workshop, HASE

Y2 - 11 August 1997 through 12 August 1997

ER -