I am mainly interested in the formal verification of numerical programs, hence floating-point arithmetic and proof assistants.
Gallery of proved programs:
All those programs were proved using the Bore version of Frama-C and the 2.26 version of Why. The Coq proofs use both the PFF and the gappalib libraries for Coq results about floating-point arithmetic.
Floating-point tricks
- Sterbenz
This function computes the exact subtraction if the inputs are near enough one to another.
C code Full Coq proof - 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 Full Coq proof - 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 Full Coq proof - 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 Full Coq proof
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.
C code Screenshot of gWhy (fully automatically proved) - 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 Screenshot of gWhy (fully automatically proved)
Numerical analysis
- rec_lin2
This example was developed among the FOST project. This very simple code is a linear recurrence of order 2. A reasonable bound on the rounding error requires a complex property that expresses each rounding error (see here for more details).
C code Full Coq proof - 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 (see here for more details).
The bound on the method error of this scheme has been formally certified in Coq (see here and here for more details). As the bound on the method error (and its properties) has not yet been linked to the bound rounding error, this proof is incomplete (2 admits are left, corresponding to the bounds on the exact values taken by the scheme, and another one corresponding to a complex mathematical property).
C code Incomplete Coq proof
