Séminaire Marelle : Certifying floating-point programs

On Friday 12/06/2009, at 11h, in room Fermat Jaune.

Speaker: Ioana Pasca.

Title: Certifying floating-point programs.

  • S. Boldo, J.C. Filliatre, G. Melquiond: Combining Coq and Gappa for Certifying Floating-Point Programs (PDF)

    Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers, such as Coq, that handle a general-purpose logic but that lack proof automation for floating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.

  • S. Boldo: Floats & Ropes: a case study for formal numerical program verification (PDF)

    We present a case study of a formal verification of a numerical program that computes the discretization of a simple partial differential equation. Bounding the rounding error was tricky as the usual idea, that is to bound the absolute value of the error at each step, fails. Our idea is to find out a precise analytical expression that cancels with itself at the next step, and to formally prove the correctness of this approach.