Certificate translation for optimizing compilers

21Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free