FOST

FOST results

• Numerical analysis programs are provided by François Clément.
  All the members have deeply looked into a particular program that solves the one-dimensional acoustic wave equation by a popular finite difference numerical scheme. To prove its correctness, we developed results on:
  • the rounding error, due to floating-point inexact computations. Sylvie Boldo has developed a method to bound this error by taking advantage of the cancellations. This work was accepted at the ICALP 2009 conference (preliminary version — final version).
  • the method error, due to the discretization. All the members have worked on the formalization of the mathematical basic definitions and on the proof of the convergence of the numerical scheme. This work was accepted at the ITP 2010 conference (preliminary version as research report — final version).
    The full Coq proof is available.
  • The full proof of the real C program is now available here.
• Automatization of floating-point proofs is also a key topic. Sylvie Boldo, Jean-Christophe Filliâtre and Guillaume Melquiond have worked on the integration of the Gappa automatic tool (specialized in floating-point arithmetic) and the Coq interactive theorem prover. This work was accepted at the Calculemus 2009 conference. (preliminary version — final version).
• Formal verification of numerical programs is the basis for proving the correctness of a program. Sylvie Boldo was invited speaker on this topic at the NSV-3 workshop. (associated article).
• Formal proofs about computer arithmetic is needed for our goal. Sylvie Boldo and Guillaume Melquiond have worked on a new Coq library about floating-point arithmetic. (preliminary version).
  Link to the library.
• Current architectures support FMA (fused multiply-and-add). Sylvie Boldo and Jean-Michel Muller have worked on computing the error of a FMA. This work was accepted at the IEEE Transactions on Computers (IEEE-TC) journal. (preliminary version).
• Current architectures and compilers may give different answers due to extended registers, FMA, compiler optimizations... Sylvie Boldo and Thi Minh Tuyen Nguyen have worked on a method to cover all cases. This work was accepted at the Innovations in Systems and Software Engineering (ISSE) journal.
• Popularization is also important. Sylvie Boldo wrote two articles for )i(, a web popularization web site. One is about the fact that it is always the computer's fault. The other is about programming.