Ressource pédagogique : Preuve automatique de la sûreté de logiciels critiques

Mots-clés :
cours / présentation - Date de création : 06-12-2012
Auteur(s) : Xavier RIVAL
Partagez !

Présentation de: Preuve automatique de la sûreté de logiciels critiques

Informations pratiques sur cette ressource

Type pédagogique : cours / présentation
Niveau : master, doctorat
Durée d'exécution : 36 minutes 48 secondes
Contenu : image en mouvement
Document : video/mp4
Taille : 3.17 Go
Droits d'auteur : libre de droits, gratuit
Droits réservés à l'éditeur et aux auteurs. © Inria Paris - Rocquencourt

Description de la ressource pédagogique

Description (résumé)

Des logiciels tels que des commandes de vol d'avions doivent être d'une fiabilité totale, dans la mesure où un dysfonctionnement du calculateur de vol pourrait entraîner une catastrophe. En particulier, il serait inacceptable qu'un tel logiciel puisse produire des erreurs à l'exécution. Il est mathématiquement impossible de déterminer de manière automatique et exacte si un logiciel informatique est correct, mais il est possible d'effectuer un calcul automatique dit conservatif, qui détectera tout problème potentiel, mais risque d'échouer à prouver la correction de certains programmes qui sont pourtant justes. Je montrerai comment cela peut être effectué grâce à la théorie mathématique de l'interprétation abstraite, et je présenterai quelques applications de ce cadre de travail à des problèmes simples.  

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

  • Vérification, essai, mesure, débogage (005.14)

Thème(s)

Intervenants, édition et diffusion

Intervenants

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

Diffusion

Document(s) annexe(s) - Preuve automatique de la sûreté de logiciels critiques

Partagez !

AUTEUR(S)

  • Xavier RIVAL

EN SAVOIR PLUS

  • Identifiant de la fiche
    17331
  • Identifiant
    oai:canal-u.fr:17331
  • Schéma de la métadonnée
  • Entrepôt d'origine
    Canal-U