Sommaire
cours / présentation, démonstration
Les jeux à la rescousse de la vérification
Les bugs informatiques peuvent parfois avoir des conséquences dramatiques, que ce soit sur le plan humain ou financier... Alors comment s'assurer que les logiciels font bien ce qu'ils sont censés faire ? C'est là qu'interviennent les méthodes formelles, une approche mathématique qui permet de prouve...
Date de création :
07.09.2023Auteur(s) :
Benjamin MonmegeAccéder à la ressource :
Présentation
Informations pratiques
Langue du document : Français
Type : cours / présentation, démonstration
Niveau : enseignement supérieur
Langues : Français
Contenu : texte, image, ressource interactive
Public(s) cible(s) : apprenant
Document : Document HTML
Age attendu : 18+
Droits d'auteur : pas libre de droits, gratuit
Ce document est diffusé sous licence Creative Commons : Paternité - Pas d'utilisation commerciale - Pas de modification. http://creativecommons.org/licenses/by-nc-nd/2.0/fr/legalcode
Ce document est diffusé sous licence Creative Commons : Paternité - Pas d'utilisation commerciale - Pas de modification. http://creativecommons.org/licenses/by-nc-nd/2.0/fr/legalcode
Description de la ressource
Résumé
Les bugs informatiques peuvent parfois avoir des conséquences dramatiques, que ce soit sur le plan humain ou financier... Alors comment s'assurer que les logiciels font bien ce qu'ils sont censés faire ? C'est là qu'interviennent les méthodes formelles, une approche mathématique qui permet de prouver de manière rigoureuse que les programmes vont s’exécuter correctement. Encore mieux, on utilise désormais la théorie des jeux pour produire automatiquement des programmes corrects, à la manière de l’écriture d’un joueur artificiel dans un jeu de société !
- Granularité : grain
- Structure : atomique
"Domaine(s)" et indice(s) Dewey
- Génie Logiciel : Tests et mesure et qualité des logiciels (005.14)
Domaine(s)
- Informatique
- Génie logiciel : conception, qualité, documentation, maintenance
- Informatique
Intervenants, édition et diffusion
Intervenants
Créateur(s) de la métadonnée :
Édition
- Inria / Interstices
Diffusion
Cette ressource vous est proposée par :
Fiche technique
Identifiant de la fiche : http://ori.unit-c.fr/uid/unit-ori-wf-1-7647
Identifiant OAI-PMH : oai:www.unit.eu:unit-ori-wf-1-7647
Statut de la fiche : final
Schéma de la métadonnée : oai:uved:Cemagref-Marine-Protected-Areas
- LOMv1.0
- LOMFRv1.0
- SupLOMFRv1.0
- Voir la fiche XML
Entrepôt d'origine : UNIT
Voir aussi
03.07.2014
Description
:
Le rôle d’un système musical interactif est de jouer d’égal à égal avec des musiciens humains. Pour cela, il doit réagir en temps réel au flux audio produit par les musiciens, suivant une « partition augmentée » écrite dans un langage spécialisé qui décrit en particulier des aspects temporels, des ...
- test et vérification automatique
- système musical interactif
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