Recent Advances in Floating-point (Static) Analyses
summary
Presents a modular extension of optimization‑based rounding‑error analysis implemented inside the Daisy framework as Hugo and a functional DSL called DS2l over vectors, using first‑order Taylor expansion plus interval/branch‑and‑bound optimization and precomputed per‑procedure error specifications to avoid inlining. Evaluates on custom benchmarks: analysis completes for 67% of large looped/vector cases where other tools handle <25%, runs several× faster, yields error bounds roughly 2× looser than the most precise tools and usually within one or two orders of magnitude of measured worst cases.
AI-written summary · about
chapters (10)
- 0:00Floating-point static analysis intro
- 3:29Floating-point arithmetic background
- 9:52Rounding error analysis
- 12:22Modular and loop challenges
- 17:04Modular analysis with calls
- 25:08Error bounds and benchmarks
- 30:29Loop handling in analysis
- 36:10DSL for loop abstraction
- 41:30Limitations and future work
- 42:57Q&A
related talks
22mModular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
14mOracle-Free Repair Synthesis for Floating-Point Programs
59mUnder-approximation for Scalable Bug Detection
23mBeating the Benchmarks: Co-evolving the ISA and Development Tools
15mCost of Soundness in Mixed-Precision Tuning
21mExact Loop Bound Analysis
16mMemory-Efficient Fixpoint Computation
36mStatic Analysis of APL for Tooling and Compliance