From Formal Verification to Correctly Rounded Math Libraries
summary
Describes concrete claims and tools: a 64-bit key lock-and-key scheme plus four metadata fields per pointer to enforce spatial and temporal memory safety; an LLVM-based instrumentation pipeline that led to a verified semantics effort and the Alive checker that now Alive used by 16 companies to verify peephole optimizations; the RLIBM approach that turns correctly rounded float32 math into a linear program solved from enumerating 4 billion float32 inputs, producing fast, verifiable libm implementations integrated into LLVM.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:04Choosing PhD advisor
- 4:58Memory safety in C
- 10:33Temporal memory safety
- 17:41Formalizing LLVM in Coq
- 21:35Automated formal verification
- 23:20Alive project
- 25:31Fast math pitfalls
- 28:20Floating-point errors in ML
- 31:08Correctly rounded math libraries
- 35:47ARM project approach
- 40:41Impact of correctly rounded functions
- 41:44Linear programming solvers
- 43:10Key takeaways
- 46:19Q&A on PhD selection
- 50:37Q&A on math functions adoption
- 53:27Q&A on verification methods
- 56:02Q&A on accuracy improvements
related talks
26mGenerating Correctly Rounded Math Libraries for New Floating Point Variants
22mCorrectly Rounded Math Libraries without Worrying about the Application’s Rounding Mode
22mOne Polynomial Approximation to Produce Correctly Rounded Results of an Elementa
58mPortable floating-point calculations
22mReconciling High-level Optimizations and Low-level Code in LLVM
01h 06mVerifying a compiler through equational means
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
24mGenerating BPF Verifier Friendly Code with Clang