Abstract
We have formal verified a number of algorithms for evaluating transcendental functions in double-extended precision floating point arithmetic in the Intel® IA-64 architecture. These algorithms are used in the Itanium™ processor to provide compatibility with IA-32 (x86) hard-ware transcendentals, and similar ones are used in mathematical software libraries. In this paper we describe in some depth the formal verification of the sin and cos functions, including the initial range reduction step. This illustrates the different facets of verification in this field, covering both pure mathematics and the detailed analysis of floating point rounding.
Cite
CITATION STYLE
Harrison, J. (2000). Formal verification of floating point trigonometric functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1954, pp. 217–233). Springer Verlag. https://doi.org/10.1007/3-540-40922-x_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
