Les jeux
à la rescousse de la vérification
Intestices

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é !

La vérification est un domaine de l’informatique ayant pour objectif d’assurer la sûreté d’un système logiciel (un programme informatique par exemple) ou matériel (un processeur d’ordinateur), c’est-à-dire que celui-ci fait bien ce que l’on veut. C’est particulièrement crucial pour des systèmes critiques, c’est-à-dire dont les défaillances causeraient des conséquences dramatiques, tant financières, humaines qu’environnementales. La vérification, c’est donc les techniques mises en œuvre pour éviter les bugs, ces fameux écrans bleus ou arrêts inopinés d’un logiciel (ce qui n’arrive, bien sûr, que le jour où nous avions oublié d’enregistrer récemment notre travail !).

Continuer à lire l’article

En savoir plus sur Interstices :

Interstices est une revue de culture scientifique en ligne, créée par des scientifiques pour vous inviter à explorer les sciences du numérique.

Interstices est publiée par Inria, institut national de recherche en sciences et technologies du numérique, elle a été lancée en 2004 à son initiative. Le suivi scientifique de la revue est assuré par le comité éditorial, qui rassemble des personnes d’Inria, du CNRS, de plusieurs universités ainsi que des associations professionnelles du domaine, notamment la SIF et la SMAI.