Faire un don ! | | style | statistiques | contactez-nous | plan | lettre d'information

Liens connexes

Dépêche modérée par

Dépêche éditée par

Articles : Prix Turing 2007 : le "Model checking" a vaincu

Posté par alenvers (). Modéré le 05 février 2008.
Presse
Le prix Turing, l'une des plus prestigieuses récompenses sinon la plus prestigieuse dans le domaine de l'informatique, vient d'être décerné à Edmund M. Clarke (de l'université Carnegie Mellon), E. Allen Emerson (Université du Texas) , et Joseph Sifakis (Université de Grenoble, laboratoire Verimag) pour leur travaux sur le "model checking".

Le "model checking" (tel que connu aujourd'hui) a émergé au début des années 1980 avec les travaux de nos trois primés. Ces travaux ont été les initiateurs d'une nouvelle discipline. De nombreux chercheurs et laboratoires leur ont emboîté le pas et le domaine est très rapidement devenu une matière de recherche importante. Cette matière fait partie désormais partie intégrante du cursus de base de toutes les études universitaires en informatique.

Vous trouverez plus de détail dans l'article complet.

> Lire la dépêche (26 commentaires, moyenne: 3,8).  

Le model checking fait partie de la famille des méthodes de vérification automatisées. Cela consiste à vérifier algorithmiquement une propriété ou un ensemble de propriétés d'un modèle par rapport à tous les états possibles d'un programme et ce à partir d'un ensemble d'états de départ. Le modèle est donc une abstraction du programme en lui-même. Cette abstraction décrit uniquement ce qui est à vérifier et est par conséquent, en quelque sorte une simplification du comportement du programme. Les propriétés, le modèle sont généralement décrits par une logique temporelle, c'est-à-dire une logique avec une notion de temps (permettant, par exemple, d'exprimer des propriétés sur les états suivants/précédents d'un système).

Le "model checking" a aujourd'hui des applications dans de nombreux domaines, dont, non-exhaustivement : la détection de bugs dans les logiciels et sur le hardware, la vérification de processus industriels critiques, la vérification des processus métier.

Pour ceux qui n'ont pas peur des maux de têtes, je les invite à lire les quelques introductions sur Wikipédia (les versions anglophones sont bien meilleures) et à investiguer du côté de quelques logiciels de vérifications, par exemple Spin ou bien Mocha ou encore Java PathFinder.

Cette discussion est archivée, il n'est plus possible de laisser des commentaires.

Note : les commentaires appartiennent à ceux qui les ont postés. Nous n'en sommes pas responsables.

Et après ça ..

Posté par ПаЗaПата () le 05/02/2008 à 22:18. (lien). Évalué à 3.

Qui ose dire que la recherche Française se porte mal ?

Comment ça, on est pas vendredi ?

cursus de base ?

Posté par Olivier Pérès (page perso, ) le 05/02/2008 à 22:50. (lien). Évalué à 3.

Chez nous (Paris Sud), ça fait partie du cursus de base du master 2 recherche. Du reste, les prérequis sont assez costauds : théorie des automates, logique temporelle, probabilités (chaînes de Markov et compagnie)... Le domaine gagnerait à être mieux connu car c'est l'un de ceux où la recherche et l'industrie s'accordent à penser qu'il y a beaucoup à faire.

Le libre c'est aussi...

Posté par Ludovic RIVALLAIN (page perso, ) le 06/02/2008 à 10:34. (lien). Évalué à 10.

je les invite à lire les quelques introductions sur Wikipédia (les versions anglophones sont bien meilleures)

On peut aussi améliorer la version française de ces articles...

Revenir en haut de page