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.