Building Reliable Compilers with a Formal Methods Framework.

Nathaniel Gray, Cristian Tapus, Aleksey Nogin, and Jason Hickey.
Building Reliable Compilers with a Formal Methods Framework.
In Dr. Indrakshi Ray, editor, The 14th International Symposium on Software Reliability Engineering (ISSRE 2003). Supplementary Proceeding, pages 319–320. Chillarege Press, 2003.
PDF, PostScript.

Abstract

We present a new approach to building reliable compilers. By implementing a compiler in a general-purpose logical framework (MetaPRL) we are able to reduce dramatically the amount of trusted code and provide a semi-formal specification of the compiling stages. This simplifies the design of the compiler and it could allow for formal reasoning about the correctness of compiled programs.

Back to my publications

Last update: Tuesday, October 25, 2005 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)