Formal Methods for Computer Arithmetic

Aperçu

Nous sommes intéressés par 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 , développement de procédures de décision dédiées, spécification et vérification effectives de bibliothèques et programmes.

Members

Permanent

PhD Students

Louise Ben Salem-Knapp

Selected 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, F. Faissole, A. Chapoutot. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE TC, 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
  • C. Fumex, C. Marché, Y. Moy. Automating the verification of floating-point programs. VSTTE, 2017. HAL
  • S. Boldo, J-H. Jourdan, G. Melquiond, X. Leroy. Verified compilation of floating-point computations. JAR, 2015. HAL

Selected software

Flocq

Formalization of fixed- and floating-point arithmetic for the Coq proof assistant

CoqInterval

Coq tactics for automatically proving inequalities over real numbers

Gappa

Decision procedure for arithmetic properties of floating-point algorithms

WhyMP

Efficient C library for arbitrary-precision integer computations, formally verified and compatible with GMP

Projects

NuSCAP

Numerical Safety for Computer-Aided Proofs
ANR
2021-2025

EMC2

Extreme-scale Mathematically-based Computational Chemistry
ERC Synergy Grant

FRESCO

Fast and Reliable Symbolic Computation
ERC Consolidator Grant