Mechanized Dominator Tree Certification
summary
Claims a verified validator of fast dominator computation: an unverified implementation (Lengauer–Tarjan variant instrumented to emit a numbering) plus a low high order certificate that a verified checker in the Rocq Prover within CompCertSSA verifies, yielding soundness and completeness for dominance. Implementation extends the previous Blazy et al. validator, builds tree+interval maps and a dominance test, and runs correctly but with a measurable slowdown mostly from computing the low‑high numbering and Rocq data structures; artifacts available.
AI-written summary · about
chapters (10)
- 0:00Dominator tree certification intro
- 2:12Verified compilation context
- 5:23Parent and sibling properties
- 8:14Low high order role
- 10:00CompCert SSA implementation
- 13:15Coq formalization
- 15:21Updated interface and proofs
- 16:49Performance impact benchmark
- 17:14Conclusion and future work
- 18:36Q&A
related talks
19mSSA without Dominance for Higher-Order Programs
19mFormally Verified Superblock Scheduling
19mFormally Verifying Optimizations with Block Simulations
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective
20mA Hierarchy of Supermartingales for ω-Regular Verification
20mFrying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
18mThe Complex(ity) Landscape of Checking Infinite Descent