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

Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan. School of Computing, University of Utah, Tech Report UUCS-15-001, April, 2015.
[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.

Bibtex:

@techreport{uucs-15-001,
  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},
  institution = {School of Computing, University of Utah},
  year = {2015},
  month = {April},
  number = {UUCS-15-001},
}