Sylvie Boldo

Formalization of Mathematics

In order to formally prove the corresponding programs, we need (applied) mathematics to be formalized too. Therefore, I have been involved in several libraries of formalized mathematics.

The coq-num-analysis library (also an opam package) includes many results of numerical analysis, including the Lebesgue integration of nonnegative functions and the Lax-Milgram theorem.

François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine, and I are currently working on the formalization of the Finite Elements Methods.

With François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis, we formally proved correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors.

We developed the Coquelicot library about real analysis with Guillaume Melquiond and Catherine Lelay.

Selected publications

A Coq Formalization of Lebesgue Integration of Nonnegative Functions. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. Journal of Automated Reasoning, 2022, 66, pp.175-213.

Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis. Journal of Automated Reasoning, 2013, 50 (4), pp.423-456.

Computer Arithmetic and its

formalization

I have been involved in computer arithmetic: theorems, algorithms, and formalizations for a long time.

Recently with Claude-Pierre Jeannerod, Guillaume Melquiond, and Jean-Michel Muller, we wrote a survey on computer arithmetic:

Floating-point arithmetic. Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller. Acta Numerica, 2023, 32, pp.203-290.

At the end of 2017, Guillaume Melquiond and I published a book that provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation. Buy it here or here.

I am also developing the Flocq library in Coq about floating-point arithmetic with Guillaume Melquiond.

Selected publications

Program Verification

Related to the previous topics, I have been involved in the formal verification of numerical programs, either to define how to annotate such programs, develop new ones, or formally prove many of them with a wide range of specificities.

I also worked on the compilation on floating-point programs, either with the CompCert framework, or with an arbitrary optimizing compiler.

• Floating-point tricks

This means floating-point arithmetic specificities are heavily used in these programs.

• Sterbenz
  This function computes the exact subtraction if the inputs are near enough one to another.
  C code
• Malcolm
  This function computes the radix of the computations. Here in IEEE-754 double precision, the result is 2. But I like the while (A != (A+1)) loop.
  C code
• Dekker
  This function computes the exact error of the multiplication (with Underflow restrictions). There are also Overflow restrictions so that no infinity will be created.
  C code


• Floating-point handling

This means that these programs would give the correct answer if real arithmetic was used, but floating-point properties are needed to prove their accuracy and that no exceptional behavior occur.

• Average, Sterbenz's version
  This function computes an approximation of the average of two floating-point numbers. It was written using hints given by Sterbenz in order to prevent overflow. Accuracy is 3/2 ulp.
  C code
• Average, correct version
  This function computes the correct rounding of the average of two floating-point numbers. It gives the perfect value, while preventing overflows.
  C code
• Discriminant
  This function computes an accurate discriminant using Kahan's algorithm. The result is proved correct within 2 ulps. Overflow and Underflow restrictions are given.
  C code
• Triangle
  This function computes the area of a triangle, even if the triangle is needle-like. The algorithm is due to Kahan. The error bound is improved on Goldberg's and overflow and underflow restrictions are given.
  C code


• Numerical analysis
• rec_lin2
  This example was developed among the FOST project. This very simple code is a linear recurrence of order 2.
  C code
• dirichlet
  This example was developed among the FOST project. It is a finite difference numerical scheme for the resolution of the one-dimensional acoustic wave equation. A reasonable bound on the rounding error requires a complex property that expresses each rounding error. The bound on the method error of this scheme has also been formally certified in Coq. For this proof, we also require the Coquelicot Coq library.
  C code
• Avionics
• eps_line1
  This example is part of KB3D, an aircraft conflict detection and resolution program. The aim is to make a decision corresponding to value -1 and 1 to decide if the plane will go to its left or its right. Note that KB3D is formally proved correct using PVS and assuming the calculations are exact. However, in practice, when the value of the computation is small, the result may be inconsistent or incorrect. The proofs are here fully automatic.
  C code
• eps_line2
  This is the same example as eps_line1 except that we are independent from the execution hardware and the compilation choices (extended registers, FMA).
  C code

Selected publications

Verified Compilation of Floating-Point Computations. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. Journal of Automated Reasoning, 2015, 54 (2), pp.135-163.

Proofs of numerical programs when the compiler optimizes. Sylvie Boldo, Thi Minh Tuyen Nguyen. Innovations in Systems and Software Engineering, 2011, 7, pp.151-160.