Sciweavers

Share
POPL
2008
ACM

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

9 years 2 months ago
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
Jean-Baptiste Tristan, Xavier Leroy
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where POPL
Authors Jean-Baptiste Tristan, Xavier Leroy
Comments (0)
books