Journal : Turing award 2007 : le "Model checking" a vaincu
Posté par alenvers () le 05 février 2008
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/
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).
Vous avez demandé le commentaire #901810.
Run by 
Cette page a été générée par Templeet en 0.0581s (dont 0.0061 de SQL).
Cette page est peut-être conforme xhtml 1.0.
Information sur le site.
Précisions
Juste pour préciser : le prix Turing, c'est ce qui se fait de mieux comme prix en informatique. En gros, l'équivalent du prix Nobel d'informatique. Et c'est la première fois que c'est un chercheur d'un labo (damned, mon labo en plus !) Français qui l'obtient.
[^]Re: Précisions
Bon, c'est pas tout, mais c'est pas en moulant sur DLFP que Vérimag obtiendra un autre prix Turing ! Bon moi aussi, faut que je me remette au boulot ;-).
[^]Re: Précisions
faut penser à arrêter le champagne ;)
[^]Re: Précisions
Le prix Nevanlinna n'est pas plus prestigieux ?
http://en.wikipedia.org/wiki/Nevanlinna_Prize
[^]Re: Précisions
Non, le prix Nevanlinna est plus "jeune" et plus spécialisé sur des travaux très mathématiques autour de l'informatique.
Le prix Turing c'est le top du top. Il n'y a que des monstres dans le palmarès, et je pourrai dire dorénavant que "une fois, il a quelques années, j'ai parlé avec un prix Turing"...
Bravo M. Sifakis, bravo le Verimag !
[^]Re: Précisions
Ohla, Vérimag n'y est pour rien ! D'ailleurs, Vérimag est la "créature" de Joseph Siphakis, fondée bien après ses premiers travaux sur le model checking.
Alors, la question c'est si l'environnement Grenoblois est pour quelque chose dans le succès de notre ex-directeur. On va souhaiter que oui ;-).
[^]Re: Précisions
En tous cas, le laboratoire verimag est connu dans le monde comme étant un des plus importants dans le petit univers de la vérification. J'y ai séjourné pendant 2 mois, il y a quelques années, j'y ai vu défiler des sommités toutes les semaines. Ce fut un séjour très instructif.
[^]Re: Précisions
>>> Le prix Turing c'est le top du top
Du fait que l'ACM est une association américaine y'a pas un biais pour désigner les vainqueurs ?
Au moins le prix Nevanlinna est décerné par l'association mathématique internationale.
[^]Re: Précisions
C'est clair que quand on regarde la couleur des drapeaux sur http://fr.wikipedia.org/wiki/Prix_Turing , on peut se poser des questions ...
D'ailleurs, cette année, il y a en fait 3 prix Turing (sur le même sujet), et quand même 2 américains ...