Graph Theoretic Constructs For Program Control Flow Analysis, 1972. ,
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 verified compiler for an impure functional language, POPL'10, pp.93-106, 2010. ,
A simple, fast dominance algorithm, 2006. ,
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
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
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
Contification Using Dominators, Proc. of ICFP'01, pp.2-13, 2001. ,
Dominator Certification and Independent Spanning Trees: An Experimental Study, Experimental Algorithms, pp.284-295, 2013. ,
DOI : 10.1007/978-3-642-38527-8_26
Finding Dominators in Practice, Journal of Graph Algorithms and Applications, vol.10, issue.1, pp.69-94, 2006. ,
DOI : 10.7155/jgaa.00119
Dominator tree verification and vertex-disjoint paths, Proc. of SODA '05, pp.433-442, 2005. ,
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
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
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
Fast mergeable integer maps, Workshop on ML, pp.77-86, 1998. ,
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. ,
Introduction to Algorithms, 2009. ,
Formal verification of SSA-based optimizations for LLVM, PLDI'13, pp.175-186, 2013. ,
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
Formalizing the LLVM intermediate representation for verified program transformation, POPL'12, pp.427-440, 2012. ,