Formal verification of translation validators: a case study on instruction scheduling optimizations
Symposium on Principles of Programming Languages, pp. 17-27, 2008.
verified compilerscoq proofinstruction scheduling optimizationstranslation validationlist schedulingMore(7+)
Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of its se- mantics. This approach can be used in a verified compiler, pro- vided that validation is formally proved to be correct. We present two such validators and their Coq proofs of correctness. The val- idators a...More