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 svn version of Frama-C (≥ 7785) and the cvs version of why (≥ Feb 19th, 2010). 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
