Using checker predicates in certifying code generation

Blech, J and Grégoire, B 2009, 'Using checker predicates in certifying code generation', in Jens Knoop, Wolf Zimmermann (ed.) Proceedings of the 8th International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2009), York, United Kingdom, 22 March 2009, pp. 1-17.


Document type: Conference Paper
Collection: Conference Papers

Title Using checker predicates in certifying code generation
Author(s) Blech, J
Grégoire, B
Year 2009
Conference name COCV 2009
Conference location York, United Kingdom
Conference dates 22 March 2009
Proceedings title Proceedings of the 8th International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2009)
Editor(s) Jens Knoop, Wolf Zimmermann
Publisher Association for Computing Machinery (ACM)
Place of publication New York, United States
Start page 1
End page 17
Total pages 17
Abstract Certifying compilation is a way to guarantee the correctness of compiler runs. A certifying compiler generates for each run a proof that it has performed the compilation task correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. Our notion of compilation correctness is based on a human readable formalization of simulation of systems to ensure the same observable behavior of programs. We focus on certifying code generation translating an intermediate language into assembler code. In previous work we found out that the time spent for checking the proofs is the bottleneck of certifying compilation. We introduced the concept of checker predicates. These are formalized in an executable way within a theorem prover to increase the speed of distinct sub tasks of certificate checking. Once the checker predicates are proved correct we are able to use them instead of traditional proving techniques within our theorem prover environment. In this paper, we present a more elaborate checker predicate for proving the simulation between intermediate and assembler programs correct. In the past this task has turned out to be the most complicated and time consuming task in certificate checking. Our checker predicate uses internally a specially formalized semantics representation of programs which is particularly suited for a fast conduction of proofs in the Coq theorem prover. Using this checker predicate we are able to speed up the task of certificate checking considerably.
Subjects Computational Logic and Formal Languages
Keyword(s) Certifying Compilation
Translation Validation
Theorem Proving
Coq
Copyright notice © 2009 Association for Computing Machinery, Inc. (ACM)
ISSN 1571-0661
Versions
Version Filter Type
Access Statistics: 149 Abstract Views  -  Detailed Statistics
Created: Mon, 22 Jul 2013, 12:21:00 EST by Catalyst Administrator
© 2014 RMIT Research Repository • Powered by Fez SoftwareContact us