– FOST

FOST a pour but de développer et d'appliquer des méthodes visant à prouver formellement la correction de programmes d'analyse numérique. En particulier, nous nous intéressons à des programmes qui peuvent apparaître dans des applications critiques dont nous voulons augmenter le niveau de garantie. Beaucoup de programmes critiques proviennent du calcul scientifique, mais peu de gens s'intéressent à leur appliquer des méthodes formelles. Une raison est que les méthodes formelles étaient trop immatures pour s'attaquer à de tels problèmes. Elles ne le sont plus et les systèmes formels sont désormais capables de manipuler des nombres réels et flottants, ce qui rend possible l'application de ces méthodes formelles à des programmes d'analyse numérique. Une autre raison importante est que les deux communautés sont éloignées. La communauté analyse numérique est habituée aux preuves papier des erreurs de méthode et ignorent l'erreur flottante car elle est très différente de leurs démonstrations usuelles. Ils ignorent ou ont peur des méthodes formelles, qui sont considérées trop éloignées de leur réalité. La communauté méthodes formelles est capable de manipuler des nombres réels et des propriétés mathématiques. Prouver ces dernières est souvent fastidieux et peu gratifiant, ce qui conduit à ignorer le calcul scientifique. FOST vise à proposer des méthodes réutilisables et compréhensibles par des non-spécialistes des méthodes formelles. FOST est l'association de plusieurs membres ayant des compétences variées et appropriées (analyse numériques, assistants de preuve, preuve de programme, arithmétique flottante) et avec une expérience significative dans leur domaines respectifs.