Department of Computer Science and Engineering
_______________________

HOME
Friday, December 5, 2003

AGENDA

SPEAKERS

• Ball
• Berry
• Harrison
• Hennessy
• Hudak
• Lowry
• Peyton Jones

TESTIMONIALS / COMMENTS

DICK'S ACCOUNT of CSE's early history

DIRECTIONS to World Forestry Center, 4033 S.W. Canyon Road, Portland, Oregon, including MAX information. Event is in Cheatham Hall.

REGISTER ONLINE
______________________

John Harrison has worked in formal verification and automated theorem proving since 1990, when he joined Mike Gordon's "Hardware Verification Group" (HVG) at the University of Cambridge Computer Laboratory. As well as working on the development of the HOL theorem prover, he developed a particular interest in the formalization of real analysis and its application to formal verification of floating-point hardware. His PhD in this area, "Theorem Proving with the Real Numbers", written under Mike Gordon's supervision, won a UK Distinguished Dissertation award and was published as a book. He also redesigned HOL from scratch, resulting in an alternative version called HOL Light.

After completing his PhD research in 1995, John Harrison spent a very enjoyable year at Åbo Akademi University and Turku Centre for Computer Science (TUCS) in Turku, Finland, where he was a member of Ralph Back's Programming Methods Research Group. Among other activities, he championed the "declarative" proofs of the Mizar system and showed how these could be integrated into other theorem-provers, work subsequently taken up in DECLARE, Isar and other systems.

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.

ABSTRACT:

Intel's Successes with Formal Methods

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, especially in the hardware domain where a serious error can force an expensive recall process. A high-profile example was the erratum in the floating-point division instruction of some Intel® Pentium® 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. Therefore, there is increasing interest in complementing testing by formal verification, which aims to prove mathematically that a design (though not necessarily a particular implementation) will meet its specification under all conditions.

Although the enterprise of formal verification has attracted much controversy, it is now a well-established technique for certain domains and has achieved notable successes. In this talk, I will give a general overview of Intel's formal verification activities, then focus on my own work on floating-point algorithms used in some recent Intel products.