Vérification formelle de programmes numériques: l'exemple de la moyenne

11/30/2015
Speaker(s) : Sylvie Boldo (Inria, LRI, projet Toccata)
Ma recherche se situe à la frontière de deux domaines de recherche : d’une part l’arithmétique des ordinateurs et d'autre part la preuve formelle de programmes. Le fait de rajouter des preuves certifiées par un assistant de preuves aux démonstrations d'algorithmes et de programmes utilisant les nombres flottants offre une garantie solide aux programmes numériques critiques. La méthodologie choisie est celle de la vérification déductive que l'on illustrera par plusieurs programmes pour calculer précisément et sans comportement exceptionnel la moyenne (x+y)/2 de deux nombres flottants.