Formal verification of floating point trigonometric functions

John Harrison.

Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2000. Springer LNCS 1954, pp. 217-233, 2000.

Abstract:

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 provide 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.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-fmcad2000,
        author          = "John Harrison",
        crossref        = "fmcad00",
        title           = "Formal verification of floating point
                           trigonometric functions",
        pages           = "217--233"}

@PROCEEDINGS{fmcad00,
        booktitle       = "Formal Methods in Computer-Aided Design:
                           Third International Conference {FMCAD} 2000",
        editor          = "Warren A. Hunt and Steven D. Johnson",
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 1954,
        year            = 2000}