Journal
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS
Volume 41, Issue 1, Pages -Publisher
ASSOC COMPUTING MACHINERY
DOI: 10.1145/3230733
Keywords
Floating-point arithmetic; IEEE floating-point standard; mixed-precision arithmetic; round-off error; global optimization; formal verification
Categories
Funding
- National Science Foundation [CCF 1535032, 1552975, 1643056, 1704715]
- Direct For Computer & Info Scie & Enginr
- Division of Computing and Communication Foundations [1552975, 1643056] Funding Source: National Science Foundation
- Direct For Computer & Info Scie & Enginr
- Division of Computing and Communication Foundations [1704715] Funding Source: National Science Foundation
Ask authors/readers for more resources
Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide very pessimistic overestimates, causing unnecessary verification failure. We have developed a new approach called Symbolic Taylor Expansions that avoids these problems, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. FPTaylor emits per-instance analysis certificates in the form of HOL Light proofs that can be machine checked. In this article, we present the basic ideas behind Symbolic Taylor Expansions in detail. We also survey as well as thoroughly evaluate six tool families, namely, Gappa (two tool options studied), Fluctuat, PRECiSA, Real2Float, Rosa, and FPTaylor (two tool options studied) on 24 examples, running on the same machine, and taking care to find the best options for running each of these tools. This study demonstrates that FPTaylor estimates round-off errors within much tighter bounds compared to other tools on a significant number of case studies. We also release FPTaylor along with our benchmarks, thus contributing to future studies and tool development in this area.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available