Tue 22 Oct 2024 14:00 - 14:30 at Pacific B - NSAD: Session 2 Chair(s): Thomas P. Jensen

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.

Tue 22 Oct

Displayed time zone: Pacific Time (US & Canada) change

14:00 - 15:30
NSAD: Session 2NSAD at Pacific B
Chair(s): Thomas P. Jensen INRIA Rennes
14:00
30m
Full-paper
A Step-Function Abstract Domain for Granular Floating-Point Error AnalysisFull Paper
NSAD
Anthony Dario University of Oregon, Samuel D. Pollard Sandia National Laboratories
DOI
14:30
30m
Full-paper
C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”Full Paper
NSAD
Rebecca Ghidini TU Munich, Julian Erhard LMU Munich; TU Munich, Michael Schwarz TU Munich, Helmut Seidl TU Munich
DOI
15:00
30m
Full-paper
Stability: An Abstract Domain for the Trend of Variation of Numerical VariablesFull Paper
NSAD
Luca Negrini Ca’ Foscari University of Venice, Sofia Presotto Ca’ Foscari University of Venice, Pietro Ferrara Ca’ Foscari University of Venice, Enea Zaffanella University of Parma, Agostino Cortesi Ca’ Foscari University of Venice
DOI