F. E. Allen, J. Cocke, I. T. Watson-research, and . Center, Graph Theoretic Constructs For Program Control Flow Analysis, 1972.

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-435, 2014.
DOI : 10.1145/2579080

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

A. Chlipala, A verified compiler for an impure functional language, POPL'10, pp.93-106, 2010.

K. D. Cooper, T. J. Harvey, and K. Kennedy, A simple, fast dominance algorithm, 2006.

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, pp.451-490, 1991.
DOI : 10.1145/115372.115320

Z. Dargaye and X. Leroy, Mechanized Verification of CPS Transformations, LPAR'07, pp.211-225, 2007.
DOI : 10.1007/978-3-540-75560-9_17

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

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

M. Fluet and S. Weeks, Contification Using Dominators, Proc. of ICFP'01, pp.2-13, 2001.

L. Georgiadis, L. Laura, N. Parotsidis, and R. E. Tarjan, Dominator Certification and Independent Spanning Trees: An Experimental Study, Experimental Algorithms, pp.284-295, 2013.
DOI : 10.1007/978-3-642-38527-8_26

L. Georgiadis, R. E. Tarjan, and R. F. Werneck, Finding Dominators in Practice, Journal of Graph Algorithms and Applications, vol.10, issue.1, pp.69-94, 2006.
DOI : 10.7155/jgaa.00119

L. Georgiadis and R. E. Tarjan, Dominator tree verification and vertex-disjoint paths, Proc. of SODA '05, pp.433-442, 2005.

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, pp.121-141, 1979.
DOI : 10.1145/357062.357071

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, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4

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

C. Okasaki and A. Gill, Fast mergeable integer maps, Workshop on ML, pp.77-86, 1998.

N. Parotsidis and L. Georgiadis, Dominators in Directed Graphs: A Survey of Recent Results, Applications, and Open Problems, 2nd International Symposium on Computing In Informatics And Mathematics (ISCIM 13), pp.15-20, 2013.

R. L. Rivest, T. H. Cormen, C. E. Leiserson, and C. Stein, Introduction to Algorithms, 2009.

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

J. Zhao and S. Zdancewic, Mechanized Verification of Computing Dominators for Formalizing Compilers, Proc. of CPP'12, pp.27-42, 2012.
DOI : 10.1007/978-3-642-35308-6_6

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