Directed Proof Generation for Machine Code
Abstract elided by the publisher.
Related papers
- Semantics-Directed Code Generation POPL 1985
- A machine-checked direct proof of the Steiner-lehmus theorem CPP 2022
- Denali: A Goal-directed Superoptimizer PLDI 2002
- Proof-directed program transformation: A functional account of efficient regular expression matching JFP 2021
- A provably sound TAL for back-end optimization PLDI 2003
- Compiler-Guaranteed Safety in Code-Copying Virtual Machines CC 2008
- Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report) ICFP 2026
- Proof-Directed De-compilation of Low-Level Code ESOP 2001