Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM
Abstract elided by the publisher.
Related papers
- AliveInLean: A Verified LLVM Peephole Optimization Verifier CAV 2019
- Alive-Infer: data-driven precondition inference for peephole optimizations in LLVM PLDI 2017
- Provably correct peephole optimizations with alive PLDI 2015
- High-Throughput, Formal-Methods-Assisted Fuzzing for LLVM CGO 2024
- Hydra: Generalizing Peephole Optimizations with Program Synthesis OOPSLA 2024
- Seamless Compiler Integration of Variable Precision Floating-Point Arithmetic CGO 2021
- LLM-VeriOpt: Verification-Guided Reinforcement Learning for LLM-Based Compiler Optimization CGO 2026
- NSan: a floating-point numerical sanitizer CC 2021