Floating point verification in HOL

John Harrison.

Proceedings of the 1995 International Workshop on Higher Order Logic theorem proving and its applications, Aspen Grove, Utah, 1995. Springer LNCS 971, pp. 186-199, 1995.

NB! This paper is updated and largely superseded by the final chapter of my PhD thesis

Abstract:

Floating-point verification is a very interesting application area for theorem provers. HOL is a general-purpose prover which is equipped with an extensive and rigorous theory of real analysis. We explain how it can be used in floating point verification, illustrating our remarks with complete verifications of simple square-root and (natural) logarithm algorithms.

DVI or PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-fp,
        crossref        = "hol95",
        author          = "John Harrison",
        title           = "Floating Point Verification in {HOL}",
        pages           = "186--199"}

@PROCEEDINGS{hol95,
        editor          = "Phillip J. Windley and Thomas Schubert and
                           Jim Alves-Foss",
        booktitle       = "Higher Order Logic Theorem Proving and Its
                           Applications: Proceedings of the 8th
                           International Workshop",
        series          = "Lecture Notes in Computer Science",
        volume          = 971,
        address         = "Aspen Grove, Utah",
        date            = "11--14 September 1995",
        year            = 1995,
        publisher       = "Springer-Verlag"}