Certifying compilation provides a means to ensure that untrusted mobile code satisfies its functional specification. A certifying compiler generates code as well as a machine-checkable "certificate", i.e. a formal proof that establishes adherence of the code to specified properties. While certificates for safety properties can be built fully automatically, certificates for more expressive and complex properties often require the use of interactive code verification. We propose a technique to provide code consumers with the benefits of interactive source code verification. Our technique, certificate translation, extends program transformations by offering the means to turn certificates of functional correctness for programs in high-level languages into certificates for executable code. The article outlines the principles of certificate translation, using specifications written in first order logic. This translation is instantiated for standard compiler optimizations in the context of an intermediate RTL Language. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Barthe, G., Grégoire, B., Kunz, C., & Rezk, T. (2006). Certificate translation for optimizing compilers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4134 LNCS, pp. 301–317). Springer Verlag. https://doi.org/10.1007/11823230_20
Mendeley helps you to discover research relevant for your work.