Formal verification of translation validators: A case study on instruction scheduling optimizations - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

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

Résumé

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.
Fichier principal
Vignette du fichier
validation-scheduling.pdf (185.11 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00289540 , version 1 (21-06-2008)

Identifiants

Citer

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⟩

Collections

INRIA INRIA2 ANR
162 Consultations
590 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More