To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 24/11/08 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                          Lundi 24 novembre, 10h30

                            -------------------
                            Guillaume Melquiond
                            -------------------

               Laboratoire commun INRIA - Microsoft Research

                   ======================================
                   Certification de programmes numériques
                   ======================================

Lors de l'évaluation précise d'une formule mathématique sur un
ordinateur, plusieurs problèmes se posent. D'une part, la formule peut
s'appuyer sur des opérateurs ou des notions absentes de l'environnement
de développement : fonctions élémentaires, équations différentielles,
etc. Une première erreur, l'erreur de modèle, est donc commise pour
adapter la formule. D'autre part, les calculs en matériel ou en logiciel
(addition, division, etc) sont rarement effectués en précision infinie
et ils divergent donc des résultats mathématiques. Les valeurs calculées
subissent alors une deuxième erreur, l'erreur d'arrondi, qui s'accumule
et se propage lors de l'évaluation.

Les calculs sont non seulement entachés d'erreurs, mais ils peuvent
aussi provoquer des comportements exceptionnels du programme : racine
carrée d'un nombre négatif, débordement, etc. Qui plus est, les domaines
des fonctions sont tellement étendus qu'ils rendent un test exhaustif
des entrées généralement impossible. Tout cela rend nécessaire une
certification des codes numériques. Réaliser cette certification à la
main est long, pénible et propice à de nombreuses erreurs qui limitent
d'autant la confiance dans les programmes. Les preuves formelles ne
souffrent pas de ce problème de confiance, mais elles sont encore plus
longues et pénibles, et généralement réservées à de rares spécialistes.

Je présenterai au cours de cet exposé quelques outils automatiques, dont
Gappa, que j'ai développés pour certifier formellement des programmes
numériques. Ils sont conçus pour être accessibles à des développeurs qui
ne sont pas spécialistes des méthodes formelles. Gappa a ainsi été
employé pour certifier des codes de plusieurs bibliothèques : CRlibm,
FLIP, CGAL... Il peut aussi être utilisé depuis l'assistant de preuves
Coq ou l'architecture de certification Why.