GT Pequan
Vérification formelle de programmes numériques: l'exemple de la moyenne
30/11/2015Intervenant(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.
Plus d'informations ici
marc (at)
nullmezzarobba.net
