Abstract
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 paper, 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.
Citation
Alexey Solovyev,
Marek Baranowski,
Ian Briggs,
Charles Jacobsen,
Zvonimir Rakamaric,
Ganesh Gopalakrishnan
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
ACM Transactions on Programming Languages and Systems (TOPLAS), 41(1): 2:1--2:39, doi:10.1145/3230733, 2018.
BibTeX
@article{2018_toplas_sbbjrg,
title = {Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions},
author = {Alexey Solovyev and Marek Baranowski and Ian Briggs and Charles Jacobsen and Zvonimir Rakamaric and Ganesh Gopalakrishnan},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
volume = {41},
publisher = {ACM},
pages = {2:1--2:39},
doi = {10.1145/3230733},
number = {1},
month = {dec},
issue_date = {March 2019},
year = {2018}
}
Acknowledgements
This work was supported by the National Science Foundation awards CCF 1535032, 1552975, 1643056, and 1704715. We would like to thank Nelson Beebe, Wei-Fan Chiang, and John Harrison for their feedback and encouragement.