X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, PLDI 2011: Programming Language Design and Implementation, pp.283-294, 2011.

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetical expressions, Mathematical Aspects of Computer Science, ser. Proc. of Symposia in Applied Mathematics, pp.33-41, 1967.

R. Milner and R. Weyrauch, Proving compiler correctness in a mechanized logic, Proc. 7th Annual Machine Intelligence Workshop, ser. Machine Intelligence, pp.51-72, 1972.

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

A. Pnueli, O. Strichman, and M. Siegel, Translation validation for synchronous languages, ICALP'98: Automata, Languages and Programming, ser. LNCS, pp.235-246, 1998.
DOI : 10.1007/BFb0055057

T. Braibant and A. Chlipala, Formal Verification of Hardware Synthesis, CAV 2013: Computer Aided Verification, ser, pp.213-228, 2013.
DOI : 10.1007/978-3-642-39799-8_14
URL : https://hal.archives-ouvertes.fr/hal-00776876