Formal Methods for Computer Arithmetic


We are interested in the use of formal methods for verifying algorithms that handle numerical values, be they floating-point numbers as described by the IEEE-754 standard, arbitrary-precision integer as in GMP, or intervals. These algorithms range from basic blocks of mathematical libraries to whole programs for numerical analysis. They are usually simple when it comes to control flow and data structures, but their correctness might depend on some intricate mathematical reasoning in number theorem, real analysis, and so on. This makes their verification out of range of purely automatic approaches.

We cover a wide range of aspects of the field: formalization of arithmetic and analysis, design of dedicated decision procedures, specification and verification of libraries and programs.



PhD Students

Paul Geneau de Lamarliere

Paul Geneau de Lamarliere

Josué Moreau

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


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


Coq tactics for automatically proving inequalities over real numbers


Decision procedure for arithmetic properties of floating-point algorithms


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



Numerical Safety for Computer-Aided Proofs


Extreme-scale Mathematically-based Computational Chemistry
ERC Synergy Grant


Fast and Reliable Symbolic Computation
ERC Consolidator Grant