Jean-Baptiste Tristan and Xavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In POPL 2008: 35th symposium Principles of Programming Languages, pages 17--27. ACM, 2008.

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.

bib | DOI | Local copy | At publisher's site ] Back


This file was generated by bibtex2html 1.99.