Formal verification of translation validators: a case study on instruction scheduling optimizations

Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of its semantics. This approach can be used in a verified compiler, provided that validation is formally proved to be correct. We present two such validators and their Coq proofs of correctness. The validators are designed for two instruction scheduling optimizations: list scheduling and trace scheduling. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - Mechanical verification; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages - Operational semantics; D.2.4 [Software Engineering]: Software/Program Verification - Correctness proofs; D.3.4 [Programming Languages]: Processors - Optimization General Terms Languages, Verification, Algorithms Keywords Translation validation, scheduling optimizations, verified compilers, the Coq proof assistant

• Type: Conference
• Year: 2008
• Where: POPL
• Authors: Jean-Baptiste Tristan, Xavier Leroy
• Keywords: Algorithms Keywords Translation, Coq Proof Assistant, Optimization General Terms, POPL 2008, Programming Languages