Mechanized Verification of Computing Dominators for Formalizing Compilers
From MaRDI portal
Publication:4916051
DOI10.1007/978-3-642-35308-6_6zbMath1383.68020OpenAlexW2102888019MaRDI QIDQ4916051
Steve Zdancewic, Jianzhou Zhao
Publication date: 19 April 2013
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-35308-6_6
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Finding dominators via disjoint set union ⋮ Approximating the smallest 2-vertex connected spanning subgraph of a directed graph ⋮ Dynamic Dominators and Low-High Orders in DAGs
Uses Software
Cites Work
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A formally verified compiler back-end
- Formalizing the LLVM intermediate representation for verified program transformations
- A fast algorithm for finding dominators in a flowgraph
- Global Data Flow Analysis and Iterative Algorithms
- Algorithms – ESA 2004
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Mechanized Verification of Computing Dominators for Formalizing Compilers
