Guaranteed Optimization: Proving Nullspace Properties of Compilers
Abstract elided by the publisher.
Related papers
- Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation VMCAI 2015
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant POPL 2006
- Type-Preserving Flat Closure Optimization OOPSLA 2025
- Witnessing Secure Compilation VMCAI 2020
- Towards efficient and verified virtual machines for dynamic languages CPP 2021
- Proving correctness of compiler optimizations by temporal logic POPL 2002
- Program specialization for execution monitoring JFP 2003
- Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow PLDI 2026