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

Jean-Baptiste Tristan 1, * Xavier Leroy 1
* Corresponding author
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/inria-00289540
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 11:39:30 AM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Friday, September 28, 2012 - 4:25:30 PM

File

validation-scheduling.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Jean-Baptiste Tristan, Xavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. 35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩. ⟨inria-00289540⟩

Share

Metrics

Record views

284

Files downloads

263