A. W. Appel and J. Palsberg, Modern Compiler Implementation in Java, 2002.

G. Barthe, D. Demange, and D. Pichardie, Formal verification of an ssa-based middleend for compcert, ACM Trans. Program. Lang. Syst, vol.36, issue.1, p.35, 2014.
URL : https://hal.archives-ouvertes.fr/inria-00634702

S. Blazy, D. Demange, and D. Pichardie, Validating dominator trees for a fast, verified dominance test, Interactive Theorem Proving -6th International Conference, vol.9236, pp.84-99, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01193281

B. Boissinot, F. Brandner, A. Darte, B. D. De-dinechin, and F. Rastello, A non-iterative data-flow algorithm for computing liveness sets in strict SSA programs, Programming Languages and Systems -9th Asian Symposium, vol.7078, pp.137-154, 2011.

B. Boissinot, A. Darte, F. Rastello, B. D. De-dinechin, and C. Guillon, Revisiting out-of-ssa translation for correctness, code quality and efficiency, The Seventh International Symposium on Code Generation and Optimization, pp.114-125, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00349925

B. Boissinot, S. Hack, D. Grund, B. D. De-dinechin, and F. Rastello, Fast liveness checking for ssa-form programs, Sixth International Symposium on Code Generation and Optimization (CGO 2008), pp.35-44, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00192219

,

D. Das, B. D. De-dinechin, and R. Upadrasta, Efficient liveness computation using merge sets and dj-graphs, TACO, vol.8, issue.4, p.18, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00647369

,

D. Demange and Y. F. De-retana, Mechanizing conventional SSA for a verified destruction with coalescing, Proceedings of the 25th International Conference on Compiler Construction, pp.77-87, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01378393

,

L. Georgiadis and R. E. Tarjan, Dominator tree certification and divergent spanning trees, ACM Trans. Algorithms, vol.12, issue.1, p.42, 2016.

C. Lattner and V. S. Adve, LLVM: A compilation framework for lifelong program analysis & transformation, 2nd IEEE / ACM International Symposium on Code Generation and Optimization, pp.75-88, 2004.

X. Leroy, A formally verified compiler back-end, J. Autom. Reasoning, vol.43, issue.4, pp.363-446, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00360768

X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister et al., Com-pCert -A Formally Verified Optimizing Compiler, ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016.

G. Ramalingam, On loops, dominators, and dominance frontiers, ACM Trans. Program. Lang. Syst, vol.24, issue.5, pp.455-490, 2002.

Y. K. Tan, M. O. Myreen, R. Kumar, A. C. Fox, S. Owens et al., The verified cakeml compiler backend, J. Funct. Program, vol.29, p.2

,