This program is tentative and subject to change.

Tue 22 Oct 2024 14:00 - 14:30 at Pacific C - NSAD: Session 2

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.

This program is tentative and subject to change.

Tue 22 Oct

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

14:00 - 15:30
NSAD: Session 2NSAD at Pacific C
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
14:30
30m
Full-paper
C-2PO: A Weakly Relational Pointer DomainFull Paper
NSAD
Rebecca Ghidini Technical University of Munich, Julian Erhard Technical University of Munich, Michael Schwarz Technische Universität München, Helmut Seidl Technische Universität München
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 Università Ca' Foscari, Venezia, Italy, Enea Zaffanella University of Parma, Italy, Agostino Cortesi Università Ca' Foscari Venezia