Deductive Formal Verification: How To Make Your Floating-Point Programs Behave

Sylvie Boldo 1, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Ma recherche se situe à la frontière de deux domaines de recherche: d'une part l'arithmétique des ordinateurs (c'est-à-dire la façon dont les ordinateurs calculent) 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 concernant l'arithmétique des ordinateurs et les nombres flottants offre une garantie solide aux programmes numériques critiques.
Type de document :
HDR
Computer Arithmetic. Université Paris-Sud, 2014
Liste complète des métadonnées

Littérature citée [182 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01089643
Contributeur : Sylvie Boldo <>
Soumis le : mardi 2 décembre 2014 - 09:38:12
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : mardi 3 mars 2015 - 10:41:13

Fichier

Identifiants

  • HAL Id : tel-01089643, version 1

Collections

Citation

Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Computer Arithmetic. Université Paris-Sud, 2014. 〈tel-01089643〉

Partager

Métriques

Consultations de la notice

379

Téléchargements de fichiers

525