, Modern Compiler Implementation in Java, 2002.
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
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
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. ,
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
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
,
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
,
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
,
Dominator tree certification and divergent spanning trees, ACM Trans. Algorithms, vol.12, issue.1, p.42, 2016. ,
LLVM: A compilation framework for lifelong program analysis & transformation, 2nd IEEE / ACM International Symposium on Code Generation and Optimization, pp.75-88, 2004. ,
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
Com-pCert -A Formally Verified Optimizing Compiler, ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016. ,
On loops, dominators, and dominance frontiers, ACM Trans. Program. Lang. Syst, vol.24, issue.5, pp.455-490, 2002. ,
The verified cakeml compiler backend, J. Funct. Program, vol.29, p.2 ,
,