A Step-Function Abstract Domain for Granular Floating-Point Error Analysis
summary
Presents a step-function abstract domain that models roundoff as a value-dependent error and implements it in a static analyzer for a subset of C (conditionals, arrays, arithmetic). Segment arithmetic, binade splitting, and a merge that chooses the larger error produce per-subrange bounds that improve bounds for subranges compared to Fluctuat; experiments show tightening near zero. The prototype sometimes produces very many pieces (up to 4,167 segments), so it runs about an order of magnitude slower than Fluctuat but exposes NaN handling and branch-instability effects.
AI-written summary · about
chapters (16)
- 0:00Floating-point error analysis
- 1:26Floating-point fundamentals
- 3:54Unit in the last place
- 5:19Rounding errors impact
- 6:24Binade boundaries for precision
- 7:07Abstract domain design
- 8:31Segment arithmetic
- 9:53Binade splitting handling
- 11:15Step function arithmetic
- 12:38Merging error bounds
- 13:21Static analyzer details
- 14:03Benchmark results
- 16:10Branch instability issues
- 17:54Performance trade-offs
- 18:36Conclusion and future work
- 20:41Q&A