Le turing award [1], l'une des plus prestigieuses récompenses si pas la plus prestigieuse, vient d'être décerné à Edmund M. Clarke [2] [(Carnegie Mellon University), E. Allen Emerson [3] (University of Texas) , et Joseph Sifakis [4] (université de grenoble - laboratoire verimag [5]) 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 iniciateurs 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.

Le "model checking" [6] fait partie de la famille des méthodes de vérification automatisée. Il consiste en vérification d'une propriété, d'un ensembles de propriétés, d'une modèle par rapport à tous les états possible d'un programme à partir d'un état de départ. Le modèle est une abstraction du programme en lui-même. Cette abstraction décrit uniquement ce qui est à vérifier et est par conséquent, une sorte "simplification" du comportement du programme. Les propriétés, le modèle est généralement décrit par une logique temporelle [7], c-à-d 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, non-exhausitvement : 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 [7] [6] sur wikipedia (Les versions anglophones sont bien meilleures) et quelques logiciels de vérifications, par exemple [8] [9].

[1] http://www.acm.org/press-room/news-releases/turing-award-07
[2] http://www.cs.cmu.edu/~emc/
[3] http://www.cs.utexas.edu/~emerson/
[4] http://www-verimag.imag.fr/~sifakis/
[5] http://www-verimag.imag.fr/
[6] http://fr.wikipedia.org/wiki/Model_checking
[7] http://fr.wikipedia.org/wiki/Logique_temporelle
[8] http://spinroot.com/spin/whatispin.html
[9] http://embedded.eecs.berkeley.edu/research/mocha/

> Lire le journal (14 commentaires, moyenne: 2,3).