A. Pnueli, M. Siegel, and E. Singerman, Translation validation, Lecture Notes in Computer Science, vol.1384, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

G. C. Necula, Translation validation for an optimizing compiler In: Programming Language Design and Implementation, pp.83-95, 2000.

X. Rival, Symbolic transfer function-based approaches to certified compilation, 31st symposium Principles of Programming Languages, pp.1-13, 2004.

J. B. Tristan and X. Leroy, Verified validation of Lazy Code Motion In: Programming Language Design and Implementation, pp.316-326, 2009.

J. B. Tristan and X. Leroy, Formal verification of translation validators: A case study on instruction scheduling optimizations, 35th symposium Principles of Programming Languages, pp.17-27, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00289540

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions, EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Huang, B. R. Childers, and M. L. Soffa, Catching and Identifying Bugs in Register Allocation, Static Analysis, 13th Int. Symp., SAS 2006, pp.281-300, 2006.
DOI : 10.1007/11823230_19

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

L. George and A. W. Appel, Iterated register coalescing, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.300-324, 1996.
DOI : 10.1145/229542.229546

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

A. W. Appel and L. George, Optimal spilling for CISC machines with few registers, In: Programming Language Design and Implementation, pp.243-253, 2001.

S. Blazy, B. Robillard, and A. W. Appel, Formal verification of coalescing graphcoloring register allocation, European Symposium on Programming, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00477689

H. Samet, Automatically Proving the Correctness of Translations Involving Optimized Code, 1975.

R. Leviathan and A. Pnueli, Validating software pipelining optimizations, Proceedings of the international conference on Compilers, architecture, and synthesis for embedded systems , CASES '02, pp.280-287, 2002.
DOI : 10.1145/581630.581676

L. Zuck, A. Pnueli, Y. Fang, and B. Goldberg, VOC, Electronic Notes in Theoretical Computer Science, vol.65, issue.2, pp.223-247, 2003.
DOI : 10.1016/S1571-0661(04)80393-1

C. W. Barrett, Y. Fang, B. Goldberg, Y. Hu, A. Pnueli et al., TVOC: A Translation Validator for Optimizing Compilers, Computer Aided Verification , 17th International Conference, CAV 2005, pp.291-295, 2005.
DOI : 10.1007/11513988_29

J. B. Tristan and X. Leroy, A simple, verified validator for software pipelining, 37th symposium Principles of Programming Languages, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00529836

S. Kundu, Z. Tatlock, and S. Lerner, Proving optimizations correct using parameterized program equivalence. In: Programming Language Design and Implementation, pp.327-337, 2009.

P. Briggs, K. D. Cooper, and L. Torczon, Rematerialization. In: Programming Language Design and Implementation, pp.311-321, 1992.
DOI : 10.1145/143103.143143