LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Liên kết » Các sự kiện tổ chức tại LIP6

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
Người thuyết trình : 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.
Biết thêm chi tiết
marc (at) nullmezzarobba.net
 Mentions légales
Sơ đồ site |