1. Mechanized Verification of Computing Dominators for Formalizing Compilers
- Author
-
Steve Zdancewic and Jianzhou Zhao
- Subjects
Development (topology) ,Dominance analysis ,Simple (abstract algebra) ,Dominator ,Programming language ,Computer science ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Compiler ,computer.software_genre ,Mathematical proof ,Formal verification ,computer - 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.
- Published
- 2012