Titre: Verifying Floating-Point Algorithms using Formalized Mathematics
Conférencier: Dr. John Harrison , Intel Corp., Hillsboro, OR, USA
Lieu: Concordia , Hall Building, Salle H-961-14
Date et heure: vendredi le 04 mars 2005 de 10:00 à 00:00

Résumé: 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.

Note biographique: 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 2005, and the associated code is already available from his Web page.

Voyez tous les séminaires >>>