Programme de l’UE

L’arithmétique virgule flottante, grâce à son efficacité (grande « dynamique » et opérateurs très rapides) s’est imposée en calcul scientifique. Aucun des problèmes numériques de très grande taille qui se posent quotidiennement aux ingénieurs (mécanique des fluides, calculs de structures, etc.) ne serait résoluble en temps raisonnable autrement qu’en arithmétique virgule flottante. Pourtant son caractère approché peut parfois poser problème (des erreurs d’arrondis peuvent s’accumuler). Egalement, une programmation erronée ou naïve peut rendre le comportement des programmes imprévisibles. Enfin, les utilisateurs ignorent trop souvent que depuis quelques années le comportement des opérations virgule flottante est complètement spécifié (norme IEEE 754), et qu’on peut élaborer des preuves qui utilisent ces spécifications. Ce dernier point est très important lorsque l’arithmétique virgule flottante est utilisée dans un contexte où une erreur pourrait avoir des conséquences graves (transport aérien, contrôle de processus physico/chimiques dangereux, etc.)

L’objet de ce cours est d’abord de présenter aux étudiants des propriétés « fines » de l’arithmétique virgule flottante: grâce aux spécifications de la norme IEEE 754, on peut construire et prouver des algorithmes qui permettent de faire des calculs « exacts » (ou très précis) avec cette arithmétique « approchée » (calculs exacts de sommes, de produits scalaires, mise au point d’algorithmes de division, de calcul des fonctions « transcendantes »). On se focalisera ensuite sur la possibilité d’élaborer des preuves formelles des algorithmes virgule flottante, en illustrant ce point par la formalisation dans l’assistant de preuve Coq de l’arithmétique virgule flottante.

Modalités d’examen. L’évaluation se fera par une analyse d’articles présentée par un rapport écrit et une soutenance orale, lors de laquelle des questions portant sur le cours pourront être posées.

Prérequis: un minimum de notions de logique et d’algorithmique. Les débutants complets en Coq sont les bienvenus, le cours s’adaptera à eux.

Bibliographie pour le cours

Calendrier prévisionnel

11/09, 18/09, 19/09, 25/09, 2/10, 3/10, 9/10, 16/10, 17/10, 24/10, 6/11, 7/11 [de 8h à 10h].

Intervenants

  • Jean-Michel Muller, DR CNRS (responsable)
  • Damien Pous, CR CNRS
  • Laurent Théry, CR INRIA