Première réunion

Geoff Barrett: Formal Methods Applied to a Floating-Point Number System (IEEE TSE 89), une première formalisation de la norme IEEE 754 dans le formalisme Z
Paul Miner: Defining the IEEE-854 Floating-Point Standrad in PVS (Nasa Tech) et avec Victor Carreño Specification of the IEEE-854 Floating-Point Standard in HOL and PVS (TPHOL 95), une formalisation un peu plus complète des normes 754 et 854 en HOL et PVS.
J Moore et co.: A mechanically checked proof of the AMD5 86 Floating-Point division program (IEEE TOC 98), une première preuve d'un algorithme de division dans ACL2. Peu de détails sur la preuve machine.
David Russinoff: A mechanically checked proof of correctness of the AMD K5 floating-point square root microcode (Formal Methos in System Design 98) and A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD K7 processor (Journal of Computation and Mathematics 98), une première preuve d'un algorithme de division dans ACL2. Diverses preuves d'algos où l'auteur pretend qu'il a trouvé des améliorations ainsi que des erreurs dans les algos initiaux. Les articles se composent d'une preuve papier que l'auteur dit avoir fait passer dans ACL2. Toutes les preuves même celle de la racine carrée sont faites en utilisant les rationnels.
John Harrison.: Floating point verification in HOL Light: the exponential function (Cambridge Tech Report 97), A Machine-Checked Theory of Floating Point Arithmetic (TPHOL99). Une première preuve d'un algorithme de calcul d'exponentielle. Tout le raisonnement (y compris la construction des réels et leurs propriétés!!) est construit à partir de la logique de base d'HOL.

L'ensemble de ces exemples montrent que parler d'arithmétique sur machine nécessite un effort non négligeable. Un passage obligé est la formalisation de la norme IEEE 754. Enfin pour pouvoir obtenir des résultats dans le temps imparti par l'action le choix des algorithmes cibles sera important.

L'environnement pour les preuves d'algorithmiques dans Coq

Loïc Pottier a fait une rapide présentation de Pcoq une interface pour le prouver Coq développée dans l'équipe LEMME. Il a particulièrement insisté sur:

la formalisation des réels dans Coq par Micaela Mayero et sa preuve du théorème des 3 intervalles.
la présentation en langue naturelle avec les notations mathématiques usuelles des preuves faites en Coq.

Comme exemple il a montré le début de la formalisation d'un article de Marc Daumas et Claire Finot sur les expansions flottantes.

Algorithmes chez Polka

Paul Zimmermann a fait une présentation de la bibliothèque MPFR pour le calcul à précision arbitraire que l'équipe Polka développe. Il a detaillé les différents algorithmes et leurs performances sous différentes architectures. Enfin il a présenté plus en détail un des algorithmes: le calcul de la racine carrée à la Karatsuba qu'il propose comme possible premier objectif de notre action.

Norme IEEE 754 et algorithme

Jean Michel Muller a fait une présentation de la norme IEEE 754 et de ses particuliarités. Il a ensuite présenté un certain nombre d'algorithmes classiques et a expliqué de quelle manière ils se conforment à la norme. Il a enfin fait un tour d'horizon des choses que l'on aimerait démontrer dans ce domaine.

Les discussions:

Les discussions ont porté sur les objectifs initiaux de l'action. Un point incontournable semble être la formalisation de la norme IEEE 754 dans Coq. Dans un objectif à 3 mois on se propose de faire ce travail en se basant sur l'effort de Patrick Loiseleur. Pour l'objectif à court-terme, deux algorithmes semblent se détacher: l'algorithme de Paul de calcul de racine carrée et les expansions flottantes de Marc et Claire.

Pour les aspects plus pratiques, Paul a proposé Nancy comme lieu de notre prochaine reunion. Elle se tiendra donc au LORIA le 13 et 14 juin. On a aussi décidé d'anticiper l'organisation du workshop à l'automne 2000 afin de permettre une possible réorientation des objectifs de notre action en fonction des conclusions de ce workshop. En conséquence la répartition du budget entre 2000 et 2001 a été effectuée comme suit:
Budget 2000

Post-Doc (3 mois)	55 KF
Stages	41 KF
Voyages	61 KF
Worskhop	25 KF
Total	182 KF

Budget 2001

Post-Doc (9 mois)	167 KF
Stages	71 KF
Voyages	60 KF
Worskhop	0 KF
Total	298 KF

Budget Total

Post-Doc (1 an)	222 KF
Stages	112 KF
Voyages	121 KF
Worskhop	25 KF
Total	480 KF

[Page d'accueil]

Laurent Théry