Contact English version

L'équipe ProVal s'est arrêtée à la fin août 2012, et renaît en une nouvelle équipe Toccata
Ces pages n'évoluent plus, suivez le lien ci-dessus pour les informations à jour sur notre équipe.

Preuves pour l'arithmétique à virgule flottante et l'analyse numérique

Présentation

Orientation of three points

Les activités de recherche poursuivies par l'axe « Arithmétique flottante » concernent la preuve de programmes contenant des calculs sur des nombres à virgule flottante, typiquement des nombres simple ou double précision de la norme IEEE-754.

L'arithmétique à virgule flottante est principalement utilisée pour calculer avec des nombres réels de façon approchée mais efficace. À cause d'une précision limitée, les opérations flottantes peuvent introduire des erreurs au cours des calculs numériques. La figure sur la droite illustre ce phénomène dans le cas de l'orientation de trois points représentés par la flèche orange. Les deux extrémités sur la diagonale sont fixées, tandis que le point du milieu se déplace librement. La couleur (bleu/vert/rouge) au niveau du point milieu indique l'orientation. Par exemple, quand ce point est au-dessus de la diagonale, les trois points sont orientés dans le sens anti-horaire, d'où la couleur bleue.

L'orientation des trois points peut s'obtenir en calculant le déterminant d'une matrice 2×2 et en s'intéressant à son signe (5 soustractions, 2 multiplications). Un déterminant nul signifie que les trois points sont alignés ; s'il est positif, les trois points sont orientés dans un sens ; et s'il est négatif, dans l'autre. Le signe calculé semble généralement correct, mais la partie inférieure de la figure montre que les imprécisions liées aux opérations flottantes entraîne un calcul incorrect de l'orientation pour certaines positions du point milieu, en particulier quand les trois points sont presque alignés.

What Every Computer Scientist Should Know About Floating-Point Arithmetic


Personnes

Sylvie Boldo, Guillaume Melquiond, Tuyen Nguyen, et partiellement Claude Marché et Jean-Christophe Filliâtre.

Thématiques

Arithmétique à virgule flottante

Emulation of FMA

Nous nous intéressons à la vérification d'algorithmes qui effectuent des opérations flottantes afin d'obtenir des résultats subtils. Ces algorithmes sont généralement courts mais ce qu'ils calculent ne se devine pas d'une simple lecture de leur code. En effet, ils représentent l'état de l'art et ont été raffinés encore et encore jusqu'à obtenir les meilleurs performances pour une précision donnée du résultat. Les opérations ont ainsi été réordonnées, des expressions ont été approchées, des principes d'exclusion ont été utilisés, et ainsi de suite. Ces algorithmes ont été testés en profondeur pendant leur développement, mais la plage des nombres flottants est tellement large que des tests exhaustifs sont hors de portée. C'est pourquoi nous développons des méthodes et des outils permettant de les vérifier formellement et de s'assurer que tous les comportements possibles ont bien été pris en compte.

Nous avons développé une formalisation générique de l'arithmétique à virgule flottante qui est utilisable aussi bien pour vérifier des programmes numériques que pour calculer au sein d'un assistant de preuve. Nous avons aussi vérifié formellement la correction de plusieurs algorithmes utilisés comme briques de base : calcul précis du discriminant, transformations sans erreur, émulation de l'opérateur FMA (fused-multiply-add), etc. La figure de droite présente l'algorithme émulant le FMA.

L'écriture manuelle de preuves formelles s'est révélée un succès, mais c'est une approche qui passe mal à l'échelle : la vérification d'algorithmes longs devient vite pénible et trop coûteuse en temps, même pour des experts en systèmes formels. Nous développons donc aussi des outils automatiques capable de vérifier des propriétés arithmétiques (domaines, erreur d'arrondi, etc) et d'en générer une preuve formelle.

Du fait de l'expertise mathématique et numérique dont sont issus les systèmes qui nous intéressent, la correction d'une partie seulement d'entre eux peut être automatiquement traitée. Une intervention humaine reste nécessaire pour vérifier les parties les plus subtiles. C'est pourquoi nous nous concentrons sur la coopération entre preuve interactive et outils automatiques. Étant donné un programme annoté, des obligations de preuve exprimant sa correction sont générées. Idéalement, la majorité de ces obligations seront déchargées automatiquement, par exemple à l'aide d'outils dédiés au calcul flottant. Les quelques unes restantes seront alors prouvées manuellement dans un système formel. Mais elles n'ont pas besoin pour autant d'être prouvées intégralement ; il suffit de les simplifier suffisamment pour que les outils automatiques prennent le relai.

Nos analyses prennent aussi en compte les changements de sémantiques apportés aux algorithmes numériques par l'environnement de calcul (architecture matérielle, compilateurs, etc). Par exemple, le jeu d'instruction d'un processeur peut fournir des registres flottants étendus ou des opérateurs FMA. Un compilateur risque alors d'en tirer avantage pour optimiser le code. Par conséquent, la précision des opérations flottantes à l'exécution ne correspond plus à celle prévue par l'algorithme initial, provoquant ainsi des changements de comportement.


Programmes d'analyse numérique

Nous souhaitons développer et appliquer des méthodes pour prouver formellement la correction de programmes provenant de l'analyse numérique. Cela se fait en deux temps: erreur d'arrondi et erreur de méthode. L'erreur d'arrondi correspond à l'accumulation des erreurs d'arrondi lors du calcul des valeurs. Il a fallu développer de nouvelles techniques complexes car les techniques usuelles donnaient une borne d'erreur trop importante par rapport à la réalité. L'erreur de méthode correspond aux erreurs dues à la discrétisation de l'équation aux dérivées partielles sur une grille. Les preuves mathématiques issues de la littérature se sont révélées insuffisantes et il a fallu combler quelques trous afin de finir formellement cette preuve. La principale difficulté a été la définition du O mathématique qui doit être très précis (par rapport aux notations mathématiques imprécises) et uniforme sur un intervalle.

Numerical scheme Oscillating rope

Nous avons travaillé sur l'équation des ondes acoustique en une dimension, ce qui correspond à l'oscillation d'une corde attachée à ses deux extrémités comme sur l'image de gauche. Cette équation aux dérivées partielles est approximée par un schéma aux différences finies du second ordre, aussi appelé « schéma à 3 points ». Plus précisément (voir l'image de droite), la valeur en pjk (point rouge) dépend de pj-1k-1, pjk-1, pj+1k-1 et pjk-2 (points bleus).


Développements de logiciels ou de preuves

Contrats

Publications liées à la thématique

[1] Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242-253, 2011. [ bib | DOI | full paper on HAL ]
[2] Sylvie Boldo. Floats & Ropes: a case study for formal numerical program verification. In 36th International Colloquium on Automata, Languages and Programming, volume 5556 of Lecture Notes in Computer Science - ARCoSS, pages 91-102, Rhodos, Greece, July 2009. Springer. [ bib ]
[3] Sylvie Boldo and Guillaume Melquiond. Emulation of FMA and Correctly-Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462-471, 2008. [ bib | full paper on HAL | PDF ]
[4] Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. In César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pages 14-23, Washington D.C., USA, April 2010. [ bib | full paper on HAL | PDF ]
[5] Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 59-74, Grand Bend, Canada, July 2009. Springer. [ bib ]