.png){kind=icon}
Return
Mechanized Dominator Tree Certification
.png){kind=icon}
PRE
AI
DOI：10.1145/3779031.3779107.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
In modern compilers, many optimizations and analyses, in particular those based on the SSA form, rely on dominance information, so computing dominators efficiently is an important problem. The classic algorithm to compute dominators in a control flow graph is the one designed by Lengauer and Tarjan in 1979. Other efficient algorithms have been proposed since. Previous works formally verified less efficient algorithms, and formally validated parts of the Lengauer-Tarjan algorithm, but there is no complete formal verification or validation of any of the fast algorithms computing dominators so far. In 2016, Georgiadis and Tarjan described a method to tackle these. They defined a certificate with which it becomes easy to validate dominators. Following their method, we successfully implemented and proved correct a validator of dominators in the Rocq Prover, inside the CompCertSSA verified compiler. This is the first complete mechanized certification of a fast algorithm computing dominators.
Keywords:
dominance
verified compilation
Rocq
Journal
P
IF:
0
Papers:
27
Citations:
0
Organization
Cited Papers
Formalizing the LLVM intermediate representation for verified program transformations.png)
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
OAAI
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesIF0
OAAIShareSaveShareSaveShareSaveShareSave
View more