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

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

J. O. Blech, L. Gesellensetter, and S. Glesner, Formal verification of dead code elimination in Isabelle/HOL, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp.200-209, 2005.
DOI : 10.1109/SEFM.2005.20

R. Bodík, R. Gupta, and M. L. Soffa, Complete removal of redundant expressions, PLDI '98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, pp.1-14, 1998.

S. Gulwani and G. C. Necula, A Polynomial-Time Algorithm for Global Value Numbering, Static Analysis, 11th Int. Symp., SAS 2004, pp.212-227, 2004.
DOI : 10.1007/978-3-540-27864-1_17

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

A. Kanade, A. Sanyal, and U. Khedker, A PVS Based Framework for Validating Compiler Optimizations, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), pp.108-117, 2006.
DOI : 10.1109/SEFM.2006.4

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

J. Knoop, O. Rüthing, and B. Steffen, Lazy code motion, Programming Languages Design and Implementation 1992, pp.224-234, 1992.

J. Knoop, O. Rüthing, and B. Steffen, Optimal code motion: theory and practice, ACM Transactions on Programming Languages and Systems, vol.16, issue.4, pp.1117-1155, 1994.
DOI : 10.1145/183432.183443

D. Leinenbach, W. Paul, and E. Petrova, Towards the formal verification of a C0 compiler: code generation and implementation correctness, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp.2-11, 2005.
DOI : 10.1109/SEFM.2005.51

S. Lerner, T. Millstein, and C. Chambers, Automatically proving the correctness of compiler optimizations, Programming Language Design and Implementation 2003, pp.220-231, 2003.

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, 2008.
DOI : 10.1007/s10817-009-9155-4

URL : https://hal.archives-ouvertes.fr/inria-00360768

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, 33rd symposium Principles of Programming Languages, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

X. Leroy and S. Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, pp.1-31, 2008.
DOI : 10.1007/s10817-008-9099-0

URL : https://hal.archives-ouvertes.fr/inria-00289542

X. Leroy, The CompCert verified compiler, 2004.
URL : https://hal.archives-ouvertes.fr/hal-01399482

E. Morel and C. Renvoise, Global optimization by suppression of partial redundancies, Communications of the ACM, vol.22, issue.2, pp.96-103, 1979.
DOI : 10.1145/359060.359069

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

A. Pnueli, O. Shtrichman, and M. Siegel, The Code Validation Tool (CVT), International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.2, pp.192-201, 1998.
DOI : 10.1007/s100090050027

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, TACAS '98, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

M. Rinard and D. Marinov, Credible compilation with pointers, Workshop on Run-Time Result Verification, 1999.

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.8235

B. Steffen, Property-oriented expansion, Static Analysis, Third International Symposium, SAS'96, pp.22-41, 1996.
DOI : 10.1007/3-540-61739-6_31

J. 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

A. Zaks and A. Pnueli, CoVaC: Compiler Validation by Program Analysis of the Cross-Product, FM 2008: Formal Methods, 15th International Symposium on Formal Methods, pp.35-51, 2008.
DOI : 10.1007/978-3-540-68237-0_5

L. Zuck, A. Pnueli, and R. Leviathan, Validation of optimizing compilers, 2001.

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