GT PequanRSS

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


http://www-pequan.lip6.fr/seminaire_pequan.php
30/11/2015
Intervenant(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
 Mentions légales
Carte du site |