Paper Info
Title
Certificate translation for optimizing compilers
Abstract
Proof Carrying Code provides trust in mobile code by requiring certificates that ensure the code adherence to specific conditions. The prominent approach to generate certificates for com- piled code is Certifying Compilation, that automatically generates certificates for simple safety properties. In this work, we present Certificate Translation, a novel extension for standard compilers that automatically transforms formal proofs for more expressive and complex properties of the source program to certificates for the compiled code. The article outlines the principles of certificate translation, instantiated for a non optimizing compiler and for standard compiler optimizations in the context of an intermediate RTL Language. Categories and Subject Descriptors: D.2.4 (Software/Program Verification): Formal methods; F.3.2 (Semantics of Programming Languages): Program analysis; F.3.1 (Specifying and Verifying and Reasoning about Programs): Logics of programs
Year
DOI
Venue
2009
10.1145/1538917.1538919
Static Analysis Symposium/Workshop on Static Analysis
Keywords
DocType
Volume
formal proof,nonoptimizing compiler,code adherence,mobile code,program verification,standard compiler,complex property,standard compiler optimizations,static analysis,proof-carrying code,program optimizations,novel extension,certificate translation,intermediate rtl language,compiler optimization,optimizing compiler,program optimization
Journal
31
Issue
ISSN
ISBN
5
0164-0925
3-540-37756-5
Citations 
PageRank 
References 
28
1.27
28
Authors
4
Name
Order
Citations
PageRank
Gilles Barthe12337152.36
Benjamin Grégoire281748.93
César Kunz316710.81
Tamara Rezk447522.41