logo
科言猫学术研究的AI总结
language
手机端手机端
  • Phone Feature微信小程序
简体中文简体中文
notice消息通知
博客博客
delete
arrow
返回

Mechanized Dominator Tree Certification

delete2026-01-01
delete0
PRE
AI
L
Lechenet, Jean-Christophe *
DOI：10.1145/3779031.3779107delete
delete原文链接
delete原文求助
delete分享
delete收藏
摘要

摘要

En 中文
在现代编译器中，许多优化和分析，特别是基于SSA形式的优化和分析，依赖于支配信息，因此高效计算支配集是一个重要问题。在控制流图中计算支配集的经典算法是Lengauer和Tarjan于1979年设计的算法。此后提出了其他高效算法。先前的工作正式验证了效率较低的算法，并正式验证了Lengauer-Tarjan算法的部分内容，但迄今为止，尚未有任何计算支配集的快速算法得到完整的正式验证或验证。2016年，Georgiadis和Tarjan描述了一种解决这些问题的方法。他们定义了一种证书，通过该证书可以轻松验证支配集。遵循他们的方法，我们在Rocq证明器中成功实现了支配集验证器，并在CompCertSSA验证编译器中证明了其正确性。这是首次对计算支配集的快速算法进行完整的机械化认证。
Keyword:
dominance
verified compilation
Rocq

期刊

P
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF:
0
论文数:
27
被引数:
0

机构

U
Universite Cote d'Azur
学者数:
453
论文数: 251
被引数: 9.7K
引用论文

引用论文

Finding dominators via disjoint set union
errJournal of Discrete Algorithms
IF0
err2013-11-01
err0
errOAAI
errWojciech Fraczak; Loukas Georgiadis; Andrew Miller; Robert E. Tarjan
err分享
err收藏
Finding Dominators in Practice
errJournal of Graph Algorithms and Applications
IF0
err2006-01-01
err0
errOAAI
errLoukas Georgiadis; Robert E. Tarjan; Renato F. Werneck
err分享
err收藏
Mechanized Verification of Computing Dominators for Formalizing Compilers
errLecture Notes in Computer Science
IF0
err2012-01-01
err0
PREAI
errZhao,Jianzhou; Zdancewic,Steve
err分享
err收藏
Addendum to “Dominator Tree Certification and Divergent Spanning Trees”
errACM Transactions on Algorithms
IF0
err2016-09-02
err0
PREAI
errGeorgiadis,Loukas; Tarjan,Robert E.
err分享
err收藏
Formalizing the LLVM intermediate representation for verified program transformations
errProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
IF0
err2012-01-25
err0
errOAAI
errJianzhou Zhao; Santosh Nagarakatte; Milo M.K. Martin; Steve Zdancewic
err分享
err收藏
A fast algorithm for finding dominators in a flowgraph
errACM Transactions on Programming Languages and Systems
IF0
err1979-01-01
err0
errOAAI
errThomas Lengauer; Robert Endre Tarjan
err分享
err收藏
A Formally Verified Compiler Back-end
errJournal of Automated Reasoning
IF0
err2009-11-04
err0
PREAI
errXavier Leroy
err分享
err收藏
Dominator Tree Certification and Divergent Spanning Trees
errACM Transactions on Algorithms
IF0
err2016-02-08
err0
PREAI
errGeorgiadis,Loukas; Tarjan,Robert E.
err分享
err收藏
Efficient Extensional Binary Tries
errJournal of Automated Reasoning
IF0
err2023-03-01
err0
PREAI
errAppel,Andrew W.; Leroy,Xavier
err分享
err收藏
Mechanised Semantics for Gated Static Single Assignment
errProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
IF0
err2023-01-11
err0
PREAI
errHerklotz,Yann; Demange,Delphine; Blazy,Sandrine
err分享
err收藏
学者 查看更多内容