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, doi:10.1007/978-3-319-19249-9_33, 2015.
BibTeX
@inproceedings{2015_fm_sjrg,
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)},
series = {Lecture Notes in Computer Science},
volume = {9109},
publisher = {Springer},
editor = {Nikolaj Bj{\o}rner and Frank de Boer},
pages = {532--550},
doi = {10.1007/978-3-319-19249-9_33},
year = {2015}
}
Acknowledgements
We would like to thank Nelson Beebe, Wei-Fan Chiang, John Harrison, and Madan Musuvathi for their feedback and encouragement. This work is supported in part by NSF CCF 1421726.