A Machine-Checked Theory of Floating Point Arithmetic

Abstract. Intel is applying formal verification to various pieces of mathematical software used in Merced, the first implementation of the new IA-64 architecture. This paper discusses the development of a generic floating point library giving definitions of the fundamental terms and containing formal proofs of important lemmas. We also briefly describe how this has been used in the verification effort so far.

• Type: Conference
• Year: 1999
• Where: TPHOL
• Authors: John Harrison
• Keywords: Automated Reasoning, Formal Verification, Generic Floating Point, Library Giving Definitions, TPHOL 1999