jeudi 10 avril
April | Agenda du libre | Framasoft | Léa-Linux | Lolix | JeSuisLibre | O'Reilly | Eyrolles | LinuxMag | Veni, Vidi, Libri | InLibroVeritas | LinuxGraphic
Faire un don ! | | style | statistiques | contactez-nous | plan | lettre d'information
Accueil :: Dépêches :: Archives :: Proposer une dépêche :: Journaux :: Forums :: Astuces :: Suivi :: RDF

Derniers journaux de alenvers :

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/

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

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.

s/iniciateurs/initiateurs/

Posté par alenvers () le 05/02/2008 à 11:20. (lien). Évalué à 2.

Pfu, la tâche, il doit surement encore y avoir pleins de coquilles !

  • [^]Re: s/iniciateurs/initiateurs/

    Posté par alenvers () le 05/02/2008 à 11:41. (lien). Évalué à 2.

    Ouais, bon, c'est une catastrophe finalement; pleins de mots qui manquent, verbes pas accordés en conséquence, lettres manquantes et/ou inversées, etc. Au moins, j'aurai essayé ;-)

Précisions

Posté par Matthieu Moy (page perso, ) le 05/02/2008 à 18:05. (lien). Évalué à 3.

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

    Posté par Aldoo (Jabber id, ) le 05/02/2008 à 18:38. (lien). Évalué à 2.

    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

      Posté par Marc (Jabber id, page perso, ) le 05/02/2008 à 19:03. (lien). Évalué à 1.

      faut penser à arrêter le champagne ;)

  • [^]Re: Précisions

    Posté par patrick_g (page perso, ) le 05/02/2008 à 19:39. (lien). Évalué à 2.

    Le prix Nevanlinna n'est pas plus prestigieux ?
    http://en.wikipedia.org/wiki/Nevanlinna_Prize

    • [^]Re: Précisions

      Posté par Pouce () le 05/02/2008 à 20:54. (lien). Évalué à 1.

      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

        Posté par Aldoo (Jabber id, ) le 05/02/2008 à 21:37. (lien). Évalué à 3.

        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

          Posté par alenvers () le 06/02/2008 à 08:53. (lien). Évalué à 3.

          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

        Posté par patrick_g (page perso, ) le 06/02/2008 à 09:14. (lien). Évalué à 2.

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

          Posté par Matthieu Moy (page perso, ) le 06/02/2008 à 18:10. (lien). Évalué à 3.

          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 ...

XP

Posté par Benjamin G. ( Prae ) (page perso, ) le 07/02/2008 à 01:20. (lien). Évalué à 2.

Les UnitTests ne seraient-ils pas des Models Checking ?

  • [^]Re: XP

    Posté par Matthieu Moy (page perso, ) le 07/02/2008 à 15:01. (lien). Évalué à 3.

    Non, ça n'a pas grand chose à voir.

    Le model-checking, c'est une exploration exhaustive de l'espace d'états.

    Les tests, unitaires ou non, c'est un essai d'un nombre fini, et dans 99.9% des cas non-exhaustif du programme.

Revenir en haut de page

Run by Team LinuxFr

Cette page a été générée par Templeet en 0.0642s (dont 0.006 de SQL).
Cette page est peut-être conforme xhtml 1.0.
Information sur le site.