FOST

En recherche de financement

Formal Proofs of Scientific Computation Programs

FOST.jpg

FOST aims at developing and applying methods to formally prove the soundness of programs used in numerical analysis. In particular, 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. Moreover, FOST aims at providing reusable methods that are understandable by non-specialists of formal methods. 

TECHNOLOGICAL OR SCIENTIFIC INNOVATIONS

  • a gallery of formally proved numerical analysis programs;
  • a library of mathematical facts to base upon in order tobound the method error;
  • several generic methods and tools for formally proving numerical analysis programs;
  • a toolbox for computing scientists to add confidence intheir programs.
Porteur du projet
FOC TRANSMISSIONS
Partenaires industriels
SEIREL , ADC/GROUPE FAYAT, GRAND PORT MARITIME DE MARSEILLE, AUBERT ET DUVAL
Partenaires recherche
LTDS / ENI-SE, ENSI BOURGES
Budget
3 600 K€
Année de labellisation
2013