Abstract
One prerequisite to the formal verification of modern compilers is to formalize computing dominators, which enable SSA forms, advanced optimizations, and analysis. This paper provides an abstract specification of dominance analysis that is sufficient for formalizing modern compilers; it describes a certified implementation and instance of the specification that is simple to design and reason about, and also reasonably efficient. The paper also presents applications of dominance analysis: an SSA-form type checker, verifying SSA-based optimizations, and constructing dominator trees. This development is a part of the Vellvm project. All proofs and implementation have been carried out in Coq. © 2012 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Zhao, J., & Zdancewic, S. (2012). Mechanized verification of computing dominators for formalizing compilers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 27–42). https://doi.org/10.1007/978-3-642-35308-6_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
