To: seminaire@pauillac.inria.fr
From: Hugo.Herbelin@inria.fr
Subject: SEM - INRIA : LogiCal - 14/11/2000 - Paris - FR
Vous pouvez maintenant vous abonner à nos annonces de séminaires
http://pauillac.inria.fr/seminaires/subscribe.html
S E M I N A I R E
. ___
/ _ _ / _ /
/ / \ / \ / / __| /
|___ |_/ |_/ / |__ |_/ |_
___ . /
/ ___ __ /_ _ / _/ /| /| _ __ __ _ _
/ / / /_ / __| / / |/ | / \ /_ / / \ | / __|
|___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/
I N R I A - Rocquencourt
Salle de conference du Bat 8
Mardi 14 novembre, 14h
-------------
John Harrison
-------------
Intel Corporation
================================================================
Verifying floating-point algorithms using formalized mathematics
================================================================
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.