Floating-Point Verification using Theorem Proving

John Harrison.

Proceedings of SFM 2006, the 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. Springer LNCS 2965, pp. 211-242.

Abstract:

This chapter describes our work on formal verification of floating-point algorithms using the HOL Light theorem prover.

DVI, PostScript or PDF

Bibtex entry:

@INPROCCEEDINGS{harrison-sfm,
        author          = "John Harrison",
        title           = "Floating-Point Verification using Theorem Proving",
        editor          = "Marco Bernardo and Alessandro Cimatti",
        booktitle       = "Formal Methods for Hardware Verification,
                           6th International School on Formal Methods for
                           the Design of Computer, Communication, and
                           Software Systems, SFM 2006",
        address         = "Bertinoro, Italy",
        date            = "May 2006",
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 3965,
        year            = 2006,
        pages           = "211--242"}