FOST

FOST documents

• Project description
• Labellisation by Digiteo
• Preliminary version of the paper "Floats & Ropes: a case study for formal numerical program verification" accepted at the ICALP 2009 conference.
• Final version of the ICALP paper.
• Preliminary version of the paper "Combining Coq and Gappa for Certifying Floating-Point Programs" accepted at the Calculemus 2009 conference.
• Final version of the Calculemus paper.
• Coq development about the method error of the wave equation discretization.
• A research report is available about the formal proof of the method error of the wave equation discretization.
• Final version of the ITP paper.
• Invited article for the NSV-3 workshop.
• Preliminary version of the IEEE-TC paper.
• Link to the Flocq library, a new Coq library about floating-point arithmetic.
• Article presenting the Flocq library at the 20th IEEE Symposium on Computer Arithmetic.
• 18-month reports for the ANR: main report and a 2-pages scientific report (in French).
• Coq development about the full proof (method error and round-off error) of the wave equation discretization program.