Verifying Fast and Sparse SSA-Based Optimizations in Coq
No abstract available.
Related papers
- Mechanizing conventional SSA for a verified destruction with coalescing CC 2016
- Enabling Sparse Constant Propagation of Array Elements via Array SSA Form SAS 1998
- SPAS: Scalable Path-Sensitive Pointer Analysis on Full-Sparse SSA APLAS 2011
- A New Algorithm for Partial Redundancy Elimination based on SSA Form PLDI 1997
- Fast liveness checking for ssa-form programs CGO 2008
- An SSA-based algorithm for optimal speculative code motion under an execution profile PLDI 2011
- Partial redundancy elimination in SSA form TOPLAS 1999
- Formal verification of SSA-based optimizations for LLVM PLDI 2013