期刊
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS
卷 41, 期 1, 页码 -出版社
ASSOC COMPUTING MACHINERY
DOI: 10.1145/3230733
关键词
Floating-point arithmetic; IEEE floating-point standard; mixed-precision arithmetic; round-off error; global optimization; formal verification
资金
- 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
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据