Arithmétique des ordinateurs et preuves formelles

Sylvie Boldo 1, 2 Guillaume Melquiond 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é : Nous confions à nos ordinateurs de nombreux calculs (météo, simulations aéronautiques, jeux vidéos, feuilles Excel...) et nous considérons naturellement que l'ordinateur fournira une réponse juste. Malheureusement, la machine utilise une arithmétique dite flottante, qui a ses contraintes. Ainsi, chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. Ce cours montrera tout d'abord la façon dont l'ordinateur calcule, mais aussi comment compenser ou tirer partie de ces erreurs. Il présentera ensuite la notion de preuve formelle qui permet de s'assurer de la correction d'un théorème mathématique et de sa preuve. Avec cela, on pourra produire des preuves d'algorithmes qui utilisent l'arithmétique des ordinateurs.
Type de document :
Communication dans un congrès
Valérie Berthé and Christiane Frougny and Natacha Portier and Marie-Françoise Roy and Anne Siegel. École des Jeunes Chercheurs en Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30, 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00755333
Contributeur : Guillaume Melquiond <>
Soumis le : mercredi 21 novembre 2012 - 09:15:58
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : vendredi 22 février 2013 - 03:47:11

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00755333, version 1

Collections

Citation

Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. Valérie Berthé and Christiane Frougny and Natacha Portier and Marie-Françoise Roy and Anne Siegel. École des Jeunes Chercheurs en Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30, 2012. 〈hal-00755333〉

Partager

Métriques

Consultations de la notice

524

Téléchargements de fichiers

715