Computer Science Colloquium

Verifying Floating-Point Algorithms Using Formalized Mathematics

John Harrison
Intel Corporation

Friday, February 6, 2004 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html

Hosts:

Clark Barrett barrett@cs.nyu.edu, (212) 998-3105

Abstract

The complexity of computer systems continues to increase, and the task of making sure that they work correctly is becoming increasingly difficult. The consequences of failure are also becoming more serious, since a serious hardware error can necessitate an extremely expensive recall process. A high-profile example was the erratum in the floating-point division instruction of some Intel Pentium(R) processors discovered in 1994, which resulted in a cost to Intel of approximately $500M.

Although simulation and testing are excellent ways of exposing bugs, they cannot, except in very restricted systems, feasibly demonstrate their absence. Given this well-recognized inadequacy, there is increasing interest in complementing testing by formal verification. This aims to prove mathematically that a design (though not necessarily a particular implementation) will meet its specification under all conditions. The proofs involved are typically long and intricate and hence are themselves usually checked for correctness by a machine.

A problem with applying traditional formal verification techniques to sophisticated floating point algorithms is that the mathematical apparatus required is quite extensive. Even to state the correctness of a floating point sine function, for example, requires a certain body of mathematical concepts, and the correctness proof uses many classical mathematical theorems. Thus, there is a need for semi-automated theorem proving systems that can not only reason about the low-level features of the design, but also the underlying mathematics.

Traditionally, theorem proving systems such as Mizar have focused on the formalization of traditional abstract mathematics, while those like the Boyer-Moore prover have focused on lower-level verification. In our work at Intel using the HOL Light prover, we have combined an extensive formalization of pure mathematics with significant practical applications, verifying the accuracy of some of the main mathematical functions in upcoming Intel processors and software libraries. We will present some of the highlights of this work and lessons for the future.

Biography

John Harrison then returned to Cambridge and worked on a formal model of floating-point arithmetic and its application to the verification of some realistic algorithms for transcendental functions. This work attracted the attention of Intel, and in 1998 John Harrison joined the company as a Senior Software Engineer specializing in the design and formal verification of mathematical algorithms. He has formally verified and in many cases designed or redesigned numerous algorithms for mathematical functions including division, square root and trigonometric functions.

In his limited spare time over the past 8 years, John Harrison has been working on a book giving a comprehensive introduction to automated theorem proving. He hopes that this book will finally reach publication in 2004, and the associated code is already available from his Web page.


top | contact webmaster@cs.nyu.edu