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

Jean-Baptiste Tristan 1, * Xavier Leroy 1
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
35th ACM Symposium on Principles of Programming Languages (POPL 2008), Jan 2008, San Francisco, United States. ACM Press, pp.17-27, 2008, 〈10.1145/1328438.1328444〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00289540
Contributeur : Xavier Leroy <>
Soumis le : samedi 21 juin 2008 - 11:39:30
Dernière modification le : lundi 5 octobre 2015 - 16:58:39
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 16:25:30

Fichier

validation-scheduling.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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), Jan 2008, San Francisco, United States. ACM Press, pp.17-27, 2008, 〈10.1145/1328438.1328444〉. 〈inria-00289540〉

Partager

Métriques

Consultations de
la notice

212

Téléchargements du document

178