A Fast Verified Liveness Analysis in SSA Form

DOI10.1007/978-3-030-51054-1_19OpenAlexW3039064847MaRDI QIDQ5049011

David Pichardie, Sandrine Blazy, Jean-Christophe Léchenet

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_19

zbMATH Keywords

dominanceverified compilationliveness analysisSSA form

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• LLVM
• CompCert

Cites Work

• A formally verified compiler back-end
• Validating Dominator Trees for a Fast, Verified Dominance Test
• Modern Compiler Implementation in Java
• Dominator Tree Certification and Divergent Spanning Trees
• The verified CakeML compiler backend

This page was built for publication: A Fast Verified Liveness Analysis in SSA Form