A Machine-Checked Theory of Floating Point Arithmetic

John Harrison.

Proceedings of the 1999 International Conference on Theorem Proving in Higher Order Logics, Nice, France, 1999, TPHOLs'99. Springer LNCS 1690, pp. 113-130, 1999.

Abstract:

Intel is applying formal verification to various pieces of mathematical software used in Merced, the first implementation of the new IA-64 architecture. This paper discusses the development of a generic floating point library giving definitions of the fundamental terms and containing formal proofs of important lemmas. We also briefly describe how this has been used in the verification effort so far.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-hol99,
        crossref        = "hol99",
        author          = John Harrison,
        title           = "A Machine-Checked Theory of Floating Point
                           Arithmetic",
        pages           = "113--130"}

@PROCEEDINGS{hol99,
        editor          = "Yves Bertot and Gilles Dowek and Andr{\'e}
                           Hirschowitz and Christine Paulin and
                           Laurent Th{\'e}ry",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           12th International Conference, TPHOLs'99",
        series          = "Lecture Notes in Computer Science",
        volume          = 1690,
        address         = "Nice, France",
        date            = "September 1999",
        year            = 1999,
        publisher       = "Springer-Verlag"}