B. Alpern, M. N. Wegman, and F. K. Zadeck, Detecting equality of variables in programs, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, 1988.
DOI : 10.1145/73560.73561

A. W. Appel, Modern compiler implementation in ML: basic techniques, 1997.
DOI : 10.1017/CBO9780511811449

A. W. Appel, SSA is functional programming, SIGPLAN Notices, 1998.
DOI : 10.1145/278283.278285
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.3282

J. Aycock and R. N. Horspool, Simple Generation of Static Single-Assignment Form, CC'00, pp.110-124, 2000.
DOI : 10.1007/3-540-46423-9_8

G. Barthe, D. Demange, and D. Pichardie, A formally verified SSAbased middle-end -Static Single Assignment meets CompCert, ESOP 2012, pp.47-66, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01110783

J. O. Blech, S. Glesner, J. Leitner, and S. Mülling, Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL, COCV'05, 2005.
DOI : 10.1016/j.entcs.2005.02.042

B. Boissinot, A. Darte, F. Rastello, B. Dupont-de-dinechin, and C. Guillon, Revisiting Out-of-SSA Translation for Correctness, Code Quality and Efficiency, 2009 International Symposium on Code Generation and Optimization, 2009.
DOI : 10.1109/CGO.2009.19
URL : https://hal.archives-ouvertes.fr/inria-00349925

B. Boissinot, S. Hack, D. Grund, B. Dupont-de-dinechin, and F. Rastello, Fast liveness checking for ssa-form programs, Proceedings of the sixth annual IEEE/ACM international symposium on Code generation and optimization , CGO '08, 2008.
DOI : 10.1145/1356058.1356064
URL : https://hal.archives-ouvertes.fr/inria-00192219

M. M. Brandis and H. Mössenböck, Single-pass generation of static single-assignment form for structured languages, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, 1994.
DOI : 10.1145/197320.197331

P. Briggs, K. D. Cooper, T. J. Harvey, and L. T. Simpson, Practical improvements to the construction and destruction of static single assignment form, Software: Practice and Experience, vol.28, issue.8, 1998.
DOI : 10.1002/(SICI)1097-024X(19980710)28:8<859::AID-SPE188>3.0.CO;2-8

P. Briggs, K. D. Cooper, and L. T. Simpson, Value numbering, SPE, 1997.

P. Brisk, Advances in Static Single Assignment form and register allocation, 2006.

A. Chlipala, A verified compiler for an impure functional language, POPL'10, 2010.

F. Chow, S. Chan, R. Kennedy, S. Liu, R. Lo et al., A New Algorithm for Partial Redundancy Elimination Based on SSA Form, Proc. of the ACM SIGPLAN 1997 conference on Programming language design and implementation, PLDI '97, 1997.

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems, vol.13, issue.4, 1991.
DOI : 10.1145/115372.115320

Z. Dargaye and X. Leroy, Mechanized Verification of CPS Transformations, LPAR'07, 2007.
DOI : 10.1007/978-3-540-75560-9_17
URL : https://hal.archives-ouvertes.fr/inria-00289541

S. Hack, D. Grund, and G. Goos, Register Allocation for Programs in SSA-Form, CC, LNCS, 2006.
DOI : 10.1007/11688839_20

J. Knoop, D. Koschützkil, and B. Steffen, Basic-block graphs: Living dinosaurs?, LNCS, 1998.
DOI : 10.1007/BFb0026423
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.6100

J. Knoop, O. Rüthing, and B. Steffen, Lazy code motion, PLDI'92, 1992.
DOI : 10.1145/989393.989439

T. Lengauer and R. E. Tarjan, A fast algorithm for finding dominators in a flowgraph, ACM Transactions on Programming Languages and Systems, vol.1, issue.1, 1979.
DOI : 10.1145/357062.357071

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

W. Mansky and E. Gunter, A Framework for Formal Verification of Compiler Optimizations, ITP'10, 2010.
DOI : 10.1007/978-3-642-14052-5_26

Y. Matsuno and A. Ohori, A type system equivalent to static single assignment, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming , PPDP '06, 2006.
DOI : 10.1145/1140335.1140365

V. Menon, N. Glew, B. R. Murphy, A. Mccreight, T. Shpeisman et al., A verifiable SSA program representation for aggressive compiler optimization, POPL'06, 2006.

G. Necula, Translation validation for an optimizing compiler, PLDI'00, 2000.

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

L. Rideau, B. P. Serpette, and X. Leroy, Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves, Journal of Automated Reasoning, vol.13, issue.12, 2008.
DOI : 10.1007/s10817-007-9096-8
URL : https://hal.archives-ouvertes.fr/inria-00289709

V. C. Sreedhar, R. Ju, D. M. Gillies, and V. Santhanam, Translating Out of Static Single Assignment Form, SAS'99, 1999.
DOI : 10.1007/3-540-48294-6_13

M. Stepp, R. Tate, and S. Lerner, Equality-Based Translation Validator for LLVM, CAV'11, 2011.
DOI : 10.1007/BFb0054170

R. Tate, M. Stepp, Z. Tatlock, and S. Lerner, Equality saturation: a new approach to optimization, POPL'09, 2009.

J. B. Tristan, P. Govereau, and G. Morrisett, Evaluating value-graph translation validation for LLVM, PLDI'11, 2011.

J. B. Tristan and X. Leroy, Verified validation of lazy code motion, PLDI'09, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415865

J. B. Tristan and X. Leroy, A simple, verified validator for software pipelining, POPL'10, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00529836

J. Zhao, S. Nagarakatte, M. Martin, and S. Zdancewic, Formal verification of SSA-based optimizations for LLVM, PLDI'13, 2013.

J. Zhao, S. Zdancewic, S. Nagarakatte, and M. Martin, Formalizing the LLVM intermediate representation for verified program transformation, POPL'12, 2012.