Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
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 OctDisplayed 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 30mTalk | ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses SAS 2023 Pre-print | ||
09:30 30mTalk | 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 30mTalk | Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs SAS 2023 Pre-print |