A. V. Aho, M. Lam, R. Sethi, and J. D. Ullman, Compilers: principles, techniques, and tools, 2006.

A. W. Appel, Modern Compiler Implementation in ML, 1998.
DOI : 10.1017/CBO9780511811449

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

J. M. Codina, J. Llosa, and A. González, A comparative study of modulo scheduling techniques, Proceedings of the 16th international conference on Supercomputing , ICS '02, pp.97-106, 2002.
DOI : 10.1145/514191.514208

B. Goldberg, E. Chapman, C. Huneycutt, and K. Palem, Software bubbles: using predication to compensate for aliasing in software pipelines, Proceedings.International Conference on Parallel Architectures and Compilation Techniques, pp.211-221, 2002.
DOI : 10.1109/PACT.2002.1106019

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

R. A. Huff, Lifetime-sensitive modulo scheduling, Proc. of the ACM SIGPLAN '93 Conf. on Programming Language Design and Implementation, pp.258-267, 1993.
DOI : 10.1145/173262.155115
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.6852

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

S. Kundu, Z. Tatlock, and S. Lerner, Proving optimizations correct using parameterized program equivalence, Proceedings of the 2009 Conference on Programming Language Design and Implementation, pp.327-337, 2009.
DOI : 10.1145/1543135.1542513
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.348.3828

M. Lam, Software pipelining, Proc. of the ACM SIGPLAN '88 Conf. on Programming Language Design and Implementation, pp.318-328, 1988.
DOI : 10.1145/989393.989420

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

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

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

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.1803

J. Llosa, A. González, E. Ayguadé, and M. Valero, Swing modulo scheduling: A lifetime-sensitive approach, IFIP WG10.3 Working Conference on Parallel Architectures and Compilation Techniques, pp.80-86, 1996.
DOI : 10.1109/pact.1996.554030

S. S. Muchnick, Advanced compiler design and implementation, 1997.

M. O. Myreen and M. J. Gordon, Transforming Programs into Recursive Functions, Brazilian Symposium on Formal Methods, pp.185-200, 2008.
DOI : 10.1016/j.entcs.2009.05.052
URL : http://doi.org/10.1016/j.entcs.2009.05.052

G. C. 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. In Tools and Algorithms for Construction and Analysis of Systems, TACAS '98, pp.151-166, 1998.

W. Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing , Supercomputing '91, pp.4-13, 1991.
DOI : 10.1145/125826.125848

B. R. Rau, Iterative modulo scheduling, International Journal of Parallel Processing, vol.24, issue.1, pp.1-102, 1996.
DOI : 10.1007/bf03356742
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.304.8660

B. R. Rau, M. S. Schlansker, and P. P. Timmalai, Code generation schema for modulo scheduled loops, 1992.

R. Tate, M. Stepp, Z. Tatlock, and S. Lerner, Equality saturation: a new approach to optimization, 36th symposium Principles of Programming Languages, pp.264-276, 2009.

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

J. Tristan and X. Leroy, Verified validation of Lazy Code Motion, Proceedings of the 2009 Conference on Programming Language Design and Implementation, pp.316-326, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415865

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

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