FOST aims at developing and applying methods to formally prove the soundness of programs used in numerical analysis.
After the success of the CerPAN ANR project (2005-2008), we are interested in programs which often appear in the resolution of critical problems and in increasing their safety level. Many critical programs come from numerical analysis, but few people have ever tried to apply formal methods to this kind of programs.
One reason is that formal methods were too immature to handle such problems. Formal method tools and in particular formal proof systems are becoming mature and are now able to deal with the real numbers and with floating-point numbers, which makes it possible to apply these systems to numerical analysis programs.
Another main reason is that the communities are apart and seldom talk one to another. The numerical analysis community are used to prove with pen and paper that their method error is bounded. They usually discard the floating-point error as it is very different from what they are used to bound. They either do not know about or are afraid of formal method, which are considered too far away their usage. The formal methods community is now able to handle real numbers and mathematical properties. Proving these properties is often tedious and hardly rewarding. Therefore, numerical analysis is discarded.
Moreover, FOST aims at providing reusable methods that are understandable by non-specialists of formal methods. FOST is the association of several members with varied and appropriate competences (numericians, experts in proof assistant design, in proofs of programs, in real and floating-point numbers) and with a significant experience in their respective domains.