Precisely Tracking Floating-Point Error with a Step-Function Abstract Domain
Anthony Dario
Committee: Zena Ariola (chair), Michal Young, Hank Childs
Directed Research Project(Mar 2024)
Keywords: Floating Point, Static Analysis, Abstract Interpretation

We present a new abstract domain for analyzing the floating-point error accrued during a computation. We model the floating-point error as a step function over an interval of possible values a variable can take. This model accurately mimics the discrete nature of floating-point error by taking into account the specific properties of floating-point numbers for closer approximations of the error. We discuss the application of this domain to some specific properties and how it allows for tighter fixpoint approximation. We implement a tool utilizing the step function domain that can analyze functions written in a subset of C. We show promising experimental results that improve on state-of-the art tools for certain output values.