Formal verification of IA-64 division algorithms

John Harrison.

Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000. Springer LNCS 1869, pp. 234-251, 2000.

Abstract:

The IA-64 architecture defers floating point and integer division to software. To ensure correctness and maximum efficiency, Intel provides a number of recommended algorithms which can be called as subroutines or inlined by compilers and assembly language programmers. All these algorithms have been subjected to formal verification using the HOL Light theorem prover. As well as improving our level of confidence in the algorithms, the formal verification process has led to a better understanding of the underlying theory, allowing some significant efficiency improvements.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-div,
        author          = "John Harrison",
        crossref        = "hol00",
        title           = "Formal verification of {IA-64} division algorithms",
        pages           = "234--251"}

@PROCEEDINGS{hol00,
        editor          = "M. Aagaard and J. Harrison",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           13th International Conference, TPHOLs 2000",
        series          = "Lecture Notes in Computer Science",
        volume          = 1869,
        year            = 2000,
        publisher       = "Springer-Verlag"}