A Step-Function Abstract Domain for Granular Floating-Point Error AnalysisFull Paper
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 OctDisplayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mFull-paper | A Step-Function Abstract Domain for Granular Floating-Point Error AnalysisFull Paper NSAD DOI | ||
14:30 30mFull-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 30mFull-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 |