Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
summary
An optimization-based static analysis extends FB Taylor to handle non-recursive procedural floating-point code by computing procedure summaries as functions of inputs using first-order Taylor approximations and symbolic betas for call-site instantiation. A prototype, Hugo, produces modular error specs (propagation and roundoff parts), inlines only at instantiation, and is significantly faster than full inlining on most benchmarks while yielding error bounds within the same order of magnitude; FB Taylor times out on two large procedures, and Hugo often gives tighter bounds than Daisy.
AI-written summary · about
chapters (14)
- 0:00Modular roundoff error analysis intro
- 1:51Notation and example setup
- 3:15Rounding model and FB-tailor
- 5:26FB-tailor’s two-step error
- 6:30FB-tailor limitations
- 7:15Hugo tool modular approach
- 9:47Error specification abstraction
- 11:58Instantiation and trade-offs
- 13:25Propagation and error separation
- 14:09Implementation and case studies
- 15:37Evaluation setup and tools
- 17:52Results and accuracy trade-off
- 18:14Conclusion and future
- 18:57Q&A
related talks
50mRecent Advances in Floating-point (Static) Analyses
30mModularity, Code Specialization, and Zero-Cost Abstractions for Program Verifica...
38mEdge-Free Programming
14mOracle-Free Repair Synthesis for Floating-Point Programs
15mCost of Soundness in Mixed-Precision Tuning
16mMemory-Efficient Fixpoint Computation
23mSpecifying and Verifying Future Conditions
59mUnder-approximation for Scalable Bug Detection