A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert
No abstract available.
Related papers
- Formal Verification of an SSA-Based Middle-End for CompCert TOPLAS 2014
- Semantic reasoning about the sea of nodes CC 2018
- Verified construction of static single assignment form CC 2016
- Formal verification of SSA-based optimizations for LLVM PLDI 2013
- Mechanised Semantics for Gated Static Single Assignment CPP 2023
- Java bytecode verification via static single assignment form TOPLAS 2008
- The Hot Path SSA Form: Extending the Static Single Assignment Form for Speculative Optimizations CC 2010
- Mechanizing conventional SSA for a verified destruction with coalescing CC 2016