LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » 链接 » 巴黎六大计算机科学实验室日志

GT PequanRSS

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


http://www-pequan.lip6.fr/seminaire_pequan.php
2015-11-30
报告人 : 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.
更多具体信息
marc (at) nullmezzarobba.net
 Mentions légales
网站导航 |