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

Share

Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan. 20th International Symposium on Formal Methods (FM 2015), Oslo, Norway.
[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 overestimates. Also, there are no available rigorous approaches that handle transcendental functions. We have developed a new approach called Symbolic Taylor Expansions that avoids this difficulty, 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. In addition to providing far tighter upper bounds of round-off error in a vast majority of cases, FPTaylor also emits analysis certificates in the form of HOL Light proofs. We release FPTaylor along with our benchmarks for evaluation.

Note: An extend version of this paper is available as a technical report.

Bibtex:

@inproceedings{fm2015-sjrg,
  author = {Alexey Solovyev and Charles Jacobsen and Zvonimir Rakamari\'c
    and Ganesh Gopalakrishnan},
  title = {Rigorous Estimation of Floating-Point Round-off Errors with
    {Symbolic} {Taylor} {Expansions}},
  booktitle = {Proceedings of the 20th International Symposium on Formal Methods (FM)},
  series = {Lecture Notes in Computer Science},
  volume = {9109},
  publisher = {Springer},
  editor = {Nikolaj Bj{\o}rner and Frank de Boer},
  year = {2015},
  pages = {532--550},
}