|
|
 |
 |
Last modified: 08.31.2009
This projet is now closed; it continue with FOST.
This projet is now closed; it continue with FOST.
- Slides presented at the
ARITH-18 conference:
"Formal Verification of Floating-Point programs".
- We formally proved a program computing a linear recurrence
of order 2. You can see the annotated C
program or download the annotated C
program and its Coq proof.
- SVN archive.
- Preliminary version of the paper "Floats & Ropes: a
case study for formal numerical program verification" accepted
at the ICALP 2009 conference.
- Preliminary version of the paper "Combining Coq and Gappa for Certifying Floating-Point Programs" accepted at the Calculemus 2009 conference.