We have formal verified a number of algorithms for
evaluating transcendental functions in double-extended
precision floating point arithmetic in the Intel (R)
IA-64 architecture. These algorithms are used in the
Itanium (TM) processor to prove compatibility with
IA-32 (x86) hardware 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.
