Formal Methods for Computer Arithmetic

Overview

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.

Members

Permanent

PhD Students

Selected publications

• P. Bonnot, B. Boyer, F. Faissole, C. Marché, R. Rieu-Helft. Formally verified rounding errors of the logarithm-sum-exponential function. FMCAD, 2024. HAL
• É. Martin-Dorel, G. Melquiond, P. Roux. Enabling floating-point arithmetic in the Coq proof assistant. JAR, 2023. HAL
• S. Boldo, C.-P. Jeannerod, G. Melquiond, J.-M. Muller. Floating-point arithmetic. Acta Numerica, 2023. HAL
• S. Boldo, F. Clément, F. Faissole, V. Martin, M. Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. JAR, 2022. HAL
• G. Melquiond, R. Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. ISSAC, 2020. HAL
• S. Boldo, G. Melquiond. Computer arithmetic and formal proofs: Verifying floating-point algorithms with the Coq System. ISTE-Elsevier, 2018. HAL
• J-M. Muller et al. Handbook of floating-point arithmetic. Birkhaüser, 2010, 2018. HAL

Full list on HAL: https://hal.science/LMF-AR

Selected software

Projects