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; available analyses computing guaranteed absolute error bounds effectively consider only monolithic straight-line code. This paper extends the roundoff error analysis based on symbolic Taylor error expressions to non-recursive procedural floating-point programs. Our analysis achieves modularity and at the same time reasonable accuracy by automatically computing abstract procedure summaries that are a function of the input parameters. We show how to effectively use first-order Taylor approximations to compute precise procedure summaries, and how to integrate these 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.