A Step-Function Abstract Domain for Granular Floating-Point Error Analysis (Video, NSAD 2024)
Anthony Dario and Samuel D. Pollard
(University of Oregon, USA; Sandia National Laboratories, USA)
Abstract: The pitfalls of numerical computations using floating-point numbers are well known. Existing static techniques for float- ing-point error analysis provide a single upper bound across all potential values for a floating-point variable. We present a new abstract domain for floating-point error analysis which describes error as a function of each variable’s value. This domain accurately models the nature of floating-point error as dependent on the magnitude of its operands. We use this domain to effectively handle exceptional values (e.g., NaN), branch instability, and binade boundaries. The granular anal- ysis provides users with a detailed understanding of forward error. We implement the abstract domain in a tool that sup- ports analyzing a subset of C including conditionals, arrays, and arithmetic operators. We compare our implementation with Fluctuat and show how our analysis can improve the error bounds for subranges of possible outputs.
Article: https://doi.org/10.1145/3689609.3689997
ORCID: https://orcid.org/0009-0001-0514-5095, https://orcid.org/0000-0002-3275-4064
Video Tags: abstract interpretation, floating point, roundoff error, step functions, splashws24nsadmain-p61-p, doi:10.1145/3689609.3689997, orcid:0009-0001-0514-5095, orcid:0000-0002-3275-4064
Presentation at the NSAD 2024 conference, October 22, 2024, https://2024.splashcon.org/home/nsad-2024
Sponsored by ACM SIGPLAN, ACM SIGAda,