Publications Details

A Step-Function Abstract Domain for Granular Floating-Point Error Analysis

Dario, Anthony; Pollard, Samuel D.

The pitfalls of numerical computations using floating-point numbers are well known. Existing static techniques for floating-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 analysis provides users with a detailed understanding of forward error. We implement the abstract domain in a tool that supports 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.