Floating-Point Verification

John Harrison.

Proceedings of FM 2005: International Symposium of Formal Methods Europe (Industry Day). Springer LNCS 3582, pp. 529-532, 2005.

Also appears in special issues of Computer Science of India Communications (vol. 31 issue 2, pp. 19-22) and Journal of Universal Computer Science (vol. 13 issue 5, pp. 629-638).

Abstract:

The floating-point domain is one of the most notable industrial success stories for formal verification. We will present some of our experience in this area at Intel, as well as briefly summarizing related work. A notable feature of verification in this area is that typical state-enumeration approaches seem inadequate on their own, and must be supplemented by general theorem proving.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-iday,
        author          = "John Harrison",
        title           = "Floating-Point Verification",
        booktitle       = "FM 2005: Formal Methods, International Symposium
                           of Formal Methods Europe, Proceedings",
        editor          = "John Fitzgerald and Ian J. Hayes and
                           Andrzej Tarlecki",
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 3582,
        year            = 2005,
        pages           = "529--532"}