G. Barthe, D. Demange, and D. Pichardie, Formal Verification of an SSA-Based Middle-End for CompCert, ACM Transactions on Programming Languages and Systems, vol.36, issue.1, pp.1-4, 2014.
DOI : 10.1145/2579080

URL : https://hal.archives-ouvertes.fr/hal-01097677

S. Blazy, D. Demange, and D. Pichardie, Validating Dominator Trees for a Fast, Verified Dominance Test, Proc. of the 6th International Conference on Interactive Theorem Proving (ITP 2015), 2015.
DOI : 10.1007/978-3-319-22102-1_6

URL : https://hal.archives-ouvertes.fr/hal-01193281

J. 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, pp.33-51, 2005.
DOI : 10.1016/j.entcs.2005.02.042

B. Boissinot, S. Hack, D. Grund, and B. , Dupont de Dine hin, and F. Rastello. Fast liveness checking for SSA-form programs, Proc. of CGO '08, pp.35-44, 2008.

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, pp.114-125, 2009.
DOI : 10.1109/CGO.2009.19

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

M. Braun, S. Buchwald, S. Hack, R. Leißa, C. Mallon et al., Simple and Efficient Construction of Static Single Assignment Form, Compiler Construction, pp.102-122, 2013.
DOI : 10.1007/978-3-642-37051-9_6

P. Briggs, K. Cooper, and L. Simpson, Value numbering, SPE, vol.27, issue.6, pp.701-724, 1997.

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, pp.859-881, 1998.
DOI : 10.1002/(SICI)1097-024X(19980710)28:8<859::AID-SPE188>3.0.CO;2-8

S. Buchwald, D. Lohner, and S. Ullrich, Verified construction of static single assignment form, Proceedings of the 25th International Conference on Compiler Construction, CC 2016, pp.67-76, 2016.
DOI : 10.1145/2892208.2892211

G. J. Chaitin, M. A. Auslander, A. K. Chandra, J. Cocke, M. E. Hopkins et al., Register allocation via coloring, Computer Languages, vol.6, issue.1, pp.47-57, 1981.
DOI : 10.1016/0096-0551(81)90048-5

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

D. Demange, L. Stefanesco, and D. Pichardie, Verifying Fast and Sparse SSA-Based Optimizations in Coq, Proc. of CC'15, pp.233-252, 2015.
DOI : 10.1007/978-3-662-46663-6_12

URL : https://hal.archives-ouvertes.fr/hal-01110779

B. Dupont-de-dinechin, Using the SSA-Form in a Code Generator, Compiler Construction, pp.1-17, 2014.
DOI : 10.1007/978-3-642-54807-9_1

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

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

L. Rideau, B. 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, pp.307-326, 2008.
DOI : 10.1007/s10817-007-9096-8

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

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

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

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