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

2015_FM_FPTaylor screenshot

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.

Citation

Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Proceedings of the 20th International Symposium on Formal Methods (FM), 9109: 532--550, 2015.

BibTeX

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