SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Tue 24 Oct 2023 10:00 - 10:30 at Room I - Cost/precision trade-offs and acceleration Chair(s): Xavier Rival

Modular static program analyses improve over global whole-program analyses in terms of scalability at a tradeoff with analysis accuracy. This tradeoff has to-date not been explored in the context of sound floating-point roundoff error analyses; existing available analyses computing guaranteed absolute error bounds consider only monolithic straight-line code. This paper presents the first modular optimization-based roundoff error analysis for non-recursive procedural floating-point programs. Our analysis achieves modularity and at the same time reasonable accuracy by automatically computing procedure summaries that are a function of the input parameters. Technically, we extend an existing optimization-based roundoff error analysis and show how to effectively use first-order Taylor approximations to compute precise procedure summaries, and how to integrate those to obtain end-to-end roundoff error bounds. Our evaluation shows that compared to an inlining of procedure calls, our modular analysis is significantly faster, while nonetheless mostly computing relatively tight error bounds.

Tue 24 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Cost/precision trade-offs and accelerationSAS 2023 at Room I
Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University
09:00
30m
Talk
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
SAS 2023
Florian Frohn RWTH Aachen University, Jürgen Giesl RWTH Aachen University
Pre-print
09:30
30m
Talk
Unconstrained Variable Oracles for Faster Static Analyses
SAS 2023
Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, Italy
Pre-print
10:00
30m
Talk
Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
SAS 2023
Rosa Abbasi Boroujeni Max Planck Institute for Software Systems, Eva Darulova Uppsala University
Pre-print