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 following tools:
- Frama-C, Neon-20140301 version
- the corresponding Jessie plugin, version 2.34. It will not compile: you have to replace lib/coq/WhyFloats.v with its svn counterpart also available here.
- Why3, 0.83 version. For the eps_line2 example, you need to replace the theories/floating_point.why file of Why3 by its git counterpart also available here.
- Coq, 8.4pl4 bersion
- PFF, 8.4 version
- Flocq, 2.3 version
- Gappa, 1.1.1 version
- Gappalib, 1.0 version
- Alt-ergo, 0.95.2 version
- CVC3 2.4.1 version
- Z3 4.3.1 version
- In may proofs, the following Coq file is used.
The programs are proved either with why2 by frama-c -jessie
-jessie-atp=gui file.c or with why3 by frama-c -jessie file.c.
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 Full Coq proof using why2 Full proof using why3 - 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 using why2 - 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 using why2
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 Full proof using why3 - 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 Full proof using why3 - 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 using why2 - 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 Full proof using why3
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 Full Coq proof using why2 - 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 Full Coq proof using why2
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 Screenshot of gWhy Screenshot of Why3 - 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 Why3