Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions

Share

Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan. ACM Transactions on Programming Languages and Systems (TOPLAS), 2018.
[pdf] [bib]

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.

Bibtex:

@article{toplas2018-sbbjrg,
  author = {Alexey Solovyev and Marek S. Baranowski and Ian Briggs and
    Charles Jacobsen and Zvonimir Rakamari\'c and Ganesh Gopalakrishnan},
  title = {Rigorous Estimation of Floating-Point Round-off Errors with
    Symbolic Taylor Expansions},
  journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  year = {2018},
  publisher = {ACM},
  note = {To appear}
}