A Machine-Checked Theory of Floating Point Arithmetic

1. M. Barratt. Formal methods applied to a floating-point system. IEEE Transactions on Software Engineering, 15:611–621, 1989.

   Article  Google Scholar 

2. M. Cornea-Hasegan. Proving the IEEE correctness of iterative floating-point square root, divide and remainder algorithms. Intel Technology Journal, 1998-Q2:1–11, 1998. Available on the Web as http://developer.intel.com/technology/itj/q21998/articles/art_3.htm.

   Google Scholar 

3. M. A. Cornea-Hasegan, R. A. Golliver, and P. Markstein. Correctness proofs outline for Newton-Raphson based floating-point divide and square root algorithms. In Koren and Kornerup P. Kornerup, editors. Proceedings, 14th IEEE symposium on on computer arithmetic [10], pages 96–105.

   Google Scholar 

4. C. Dulong. The IA-64 architecture at work. IEEE Computer, 64(7):24–32, July 1998.

   Article  Google Scholar 

5. D. Goldberg. What every computer scientist should know about floating point arithmetic. ACM Computing Surveys, 23:5–48, 1991.

   Article  Google Scholar 

6. M. J. C. Gordon and T. F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993.

   Google Scholar 

7. J. Harrison. Floating point verification in HOL Light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1997.

   Google Scholar 

8. J. Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998. Revised version of author’s PhD thesis.

   Google Scholar 

9. IEEE. Standard for binary floating point arithmetic. ANSI/IEEE Standard 754-1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA, 1985.

   Google Scholar 

10. I. Koren and P. Kornerup, editors. Proceedings, 14th IEEE symposium on on computer arithmetic, Adelaide, Australia, 1999. IEEE Computer Society.

    Google Scholar 

11. P. W. Markstein. Computation of elementary functions on the IBM RISC System/6000 processor. IBM Journal of Research and Development, 34:111–119, 1990.

    Article  MathSciNet  Google Scholar 

12. P. S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical memorandum 110167, NASA Langley Research Center, Hampton, VA 23681-0001, USA, 1995.

    Google Scholar 

13. J-M. Muller. Elementary functions: Algorithms and Implementation. Birkhäuser, 1997.

    Google Scholar 

14. J. O’Leary, X. Zhao, R. Gerth, and C-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, 1999-vnQ1:1–14, 1999. Available on the Web as http://developer.intel.com/technology/itj/q11999/articles/art_5.htm.

    Google Scholar 

15. L. C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.

    Article  MathSciNet  MATH  Google Scholar 

16. D. Rusinoff. A mechanically checked proof of IEEE compliance of a registertransfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics, 1:148–200, 1998. Available on the Web via http://www.onr.com/user/russ/david/k7-div-sqrt.html.

    Article  MathSciNet  Google Scholar 

17. S. Story and P. T. P. Tang. New algorithms for improved transcendental functions on IA-64. In Koren and Kornerup P. Kornerup, editors. Proceedings, 14th IEEE symposium on on computer arithmetic, Adelaide, Australia, 1999 [10], pages 4–11.

    Google Scholar 

Download references