Méthodes formelles pour l'arithmétique des ordinateurs

Cette thématique concerne l'utilisation de méthodes formelles pour vérifier des algorithmes manipulant des valeurs numériques, que ce soit des nombres à virgule flottante de la norme IEEE 754 ou des grands entiers à la GMP ou encore des intervalles. Il peut s'agir aussi bien de briques de base de bibliothèques que de programmes complets d'analyse numérique. Ces algorithmes sont généralement simples du point de vue du flot de contrôle et des structures de données, mais la vérification de leur correction nécessite des raisonnements mathématiques subtils en théorie des nombres, analyse réelle, etc, ce qui les rend hors de portée d'approches purement automatiques. Cette thématique couvre différents aspects du domaine : formalisations de l'arithmétique et de l'analyse pour des systèmes formelles, développement de procédures de décision dédiées, spécification et vérification effectives de bibliothèques et programmes.

Membres permanents

  • Sylvie Boldo
  • Claude Marché
  • Guillaume Melquiond

Membres non-permanents

  • Raphaël Rieu-Helft
  • Diane Gallois-Wong
  • Louise Ben Salem-Knapp

Quelques publications

  • G. Melquiond, R. Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. ISSAC, 2020. HAL
  • A. Mahboubi, G. Melquiond, T. Sibut-Pinote. Formally verified approximations of definite integrals. JAR, 2019. HAL
  • S. Boldo, G. Melquiond. Computer arithmetic and formal proofs: Verifying floating-point algorithms with the Coq System. ISTE-Elsevier, 2018.
  • J-M. Muller et al. Handbook of floating-point arithmetic. Birkhaüser, 2010, 2018.
  • S. Conchon, M. Iguernelala, K. Ji, G. Melquiond, C. Fumex. A three-tier strategy for reasoning about floating-point numbers in SMT. CAV, 2017. HAL
  • S. Boldo, J-H. Jourdan, G. Melquiond, X. Leroy. Verified compilation of floating-point computations. JAR, 2015. HAL
  • C. Fumex, C. Marché, Y. Moy. Automating the verification of floating-point programs. VSTTE, 2017. HAL

Quelques développements

  • Flocq : formalisation de l'arithmétique à virgules fixe et flottante pour l'assistant de preuves Coq.
  • CoqInterval : tactiques Coq pour la preuve automatique d'inégalités sur les nombres réels.
  • Gappa : procédure de décision pour les propriétés arithmétiques en virgule flottante.
  • WhyMP : bibliothèque C efficace sur les grands entiers, vérifiée formellement et compatible avec GMP.

Projets

  • NUSCAP
  • EMC2 (ERC Synergy grant)
  • contrat avec le CEA-DAM