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 |
Externally published | Yes |
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
- General Engineering