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
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
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
Dupont de Dine hin, and F. Rastello. Fast liveness checking for SSA-form programs, Proc. of CGO '08, pp.35-44, 2008. ,
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
Simple and Efficient Construction of Static Single Assignment Form, Compiler Construction, pp.102-122, 2013. ,
DOI : 10.1007/978-3-642-37051-9_6
Value numbering, SPE, vol.27, issue.6, pp.701-724, 1997. ,
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
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
Register allocation via coloring, Computer Languages, vol.6, issue.1, pp.47-57, 1981. ,
DOI : 10.1016/0096-0551(81)90048-5
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
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
Using the SSA-Form in a Code Generator, Compiler Construction, pp.1-17, 2014. ,
DOI : 10.1007/978-3-642-54807-9_1
Register Allocation for Programs in SSA-Form, CC, LNCS, pp.247-262, 2006. ,
DOI : 10.1007/11688839_20
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
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
Translating Out of Static Single Assignment Form, SAS'99, pp.194-210, 1999. ,
DOI : 10.1007/3-540-48294-6_13
Formalizing the LLVM intermediate representation for verified program transformation, POPL'12, pp.427-440, 2012. ,
Formal verification of SSA-based optimizations for LLVM, PLDI'13, pp.175-186, 2013. ,