cours / présentation

Pourquoi mon ordinateur calcule faux?

Dans cet exposé Sylvie Boldo nous fait prendre conscience de l'importance des bugs en informatique et des conséquences historiques qu'ils ont pu engendrer. Elle se concentre ensuite sur les problèmes liés aux calculs numériques et montre de manière détaillée et constructive comment prendre la mesure...

Date de création :

16.06.2009

Auteur(s) :

Sylvie BOLDO

Présentation

Informations pratiques

Langue du document : Français
Type : cours / présentation
Niveau : formation continue
Durée d'exécution : 36 minutes
Contenu : vidéo
Document : video/mp4
Poids : 103.24 Mo
Droits d'auteur : libre de droits, gratuit
Droits réservés à l'éditeur et aux auteurs.

Description de la ressource

Résumé

Dans cet exposé Sylvie Boldo nous fait prendre conscience de l'importance des bugs en informatique et des conséquences historiques qu'ils ont pu engendrer. Elle se concentre ensuite sur les problèmes liés aux calculs numériques et montre de manière détaillée et constructive comment prendre la mesure des approximations numériques qui s'effectuent lors d'un calcul numérique au sein d'un logiciel. Elle nous offre à la fois des garde-fous pratiques et une compréhension théorique de la problématique. Cet exposé s'est inscrit dans le cadre d'une formation INRIA proposée en juin 2009 et s'adressait aux professeurs des établissements de l'académie de Versailles proposant l'option Informatique et Objets Numériques à leurs classes de seconde pour l'année scolaire 2009-2010.

"Domaine(s)" et indice(s) Dewey

  • Analyse numérique (518)
  • Vérification, essai, mesure, débogage (005.14)

Domaine(s)

  • Analyse numérique
  • Analyse numérique appliquée, calcul numérique, mathématiques numériques
  • Informatique
  • Génie logiciel : conception, qualité, documentation, maintenance
  • Informatique

Intervenants, édition et diffusion

Intervenants

Fournisseur(s) de contenus : INRIA (Institut national de recherche en informatique et automatique)

Diffusion

Cette ressource vous est proposée par :Canal-U - accédez au site internet

Document(s) annexe(s)

Fiche technique

Identifiant de la fiche : 6629
Identifiant OAI-PMH : oai:canal-u.fr:6629
Schéma de la métadonnée : oai:uved:Cemagref-Marine-Protected-Areas
Entrepôt d'origine : Canal-U

Voir aussi

UNIT
UNIT
08.10.2009
Description : Les outils de vérification formelle de programmes (analyseurs statiques, prouveurs de programmes, model-checkers) ont fait des progrès remarquables ces dernières années et commencent à percer dans le monde du logiciel critique. Cependant, ces outils ne vérifient "que" des programmes source: des ...
  • compilateur
  • logiciel critique
  • programmation fonctionnelle
  • vérification de programme
  • vérification formelle
  • preuve formelle
  • fuscia
  • conference
  • stic
  • recherche
UNIT
UNIT
21.09.2012
Description : Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique ...
  • Coq
  • assistant de preuve
  • programmation fonctionnelle sûre
  • preuve de programme
  • logique mathématique
  • méthode formelle
  • calcul des constructions
  • correction de logiciel
  • algorithmique certifiée
  • théorie des types
  • logiciel libre
  • récursion
  • fuscia