Prix Turing 2007 : le "Model checking" a vaincu

Posté par (page perso) . Modéré par Jaimé Ragnagna.
Tags : aucun
1
5
fév.
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. 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.

  • # Et après ça ..

    Posté par (page perso) . Évalué à 3.

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

    Comment ça, on est pas vendredi ?
    • [^] # Re: Et après ça ..

      Posté par . Évalué à 1.

      Si on devait comparer le "ratio" Recherche / Moyens alloués, je crois que la France se placerait sans problème dans le peloton de tête (si ce n'est LA tête).
      N'empêche que, comme d'hab', en France on commence sa réflexion, puis on s'expatrie aux States pour y faire du pognon...
      • [^] # Re: Et après ça ..

        Posté par (page perso) . Évalué à 7.

        J'ai un pote en recherche au CNRS qui touche le SMIC x 1.3 (pour bac +8officiel), comme beaucoup de chercheurs français, et il est revenu de princeton. Je suis prêt à parier que par rapport aux stats imaginaire (40% d'expat) la réalité est bien inférieure en terme de chercheurs qui "fuient la france".

        Je met un bifton de 50€ sur moins de 10% d'expat qui ne reviennent pas en france au moins une fois, malgré un salaire 2 fois inférieur à ce que l'on leur propose ailleurs.
        • [^] # Re: Et après ça ..

          Posté par . Évalué à 10.

          Á mon avis, les gens reviennent en partie à cause du statut du chercheur en France (et encore...). Mais à mon avis (qualifié, puisque je suis chercheur expat), tu reviens principalement pour des raisons non professionnelles : une grande partie de ta vie est en France, tu vois plus ta famille, tes amis, voire l'autre moitié de ton couple; tu ne reviens plus que pour les enterrements. À ajouter à ça, le problème du choc culturel (Les étrangers sont tous des cons comme dirait Desproges), la langue (il n'y a pas que les US dans la vie), le climat... Voire une petite dose de xénophobie "bien naturelle", qui fait que tu est bienvenu pour rester quelques années, mais que tu sens bien qu'avoir un poste de prof, c'est une autre paire de manches.

          Bref, si les expats reviennent en France, c'est pas à cause de la France, c'est à cause du statut d'expat. Ça ne change rien aux statistiques de retour, mais ça veut dire que l'état pourri de la rehcreche en France oblige les gens à faire un choix entre leur carrière et leur vie personelle, et à accepter des postes mal payés dans des labos miteux parce qu'ils sont attachés émotionnellement au pays dans lequel il ont grandi. Je ne trouve pas ça très sain, personnellement.
          • [^] # Re: Et après ça ..

            Posté par . Évalué à 7.

            Á mon avis, les gens reviennent en partie à cause du statut du chercheur en France (et encore...).
            Heureusement, si les recommandations d'Attali sont suivies, le statut des chercheurs en France ne vaudra plus grand chose (CDD renouvelables, et le même salaire minable qu'avant), et nos amis expats auront une raison de moins de revenir.
            • [^] # Re: Et après ça ..

              Posté par (page perso) . Évalué à 4.

              Le monsieur Attali nous explique sur le quotidien Le Monde que le CDD 3 fois renouvelable (quand t'as déjà 30 ans et bac+8,10,12 ...) c'est pas précaire :


              Nicolas : Je suis doctorant, je pars le mois suivant en post-doc' aux Etats-Unis. Je comptais postuler au CNRS, à l'Inria. Mais je viens de voir que vous proposez que les jeunes chercheurs commencent par des contrats de quatre ans renouvelables une fois. Pensez-vous réellement que cela va faire revenir les chercheurs en France ? C'est triste à dire, mais autant rester aux Etats-Unis que de rentrer pour un poste précaire.


              Jacques Attali : Vous verrez qu'aux Etats-Unis, les postes sont exactement de ce genre et que la recherche y est faite par des gens qui se remettent en cause en permanence sur leurs capacités à trouver. Un contrat de quatre ans renouvelable trois fois, ce n'est pas ce que j'appelle de la précarité.


              Ce monsieur nous apporte la solution universelle, la panacée, la martingale de la recherche!
              Notez que les chercheurs français sont des nazes qui ne se remettent pas en cause et que le CDD 3 fois renouvelable va "apporter bonheur a tous dans la recherche française"...

              Voilà la vieille idée qui consiste à dire que si on tiens les gens par les couilles, ils vont avancer plus vite.
              Je suggère d'appliquer ça aux checheurs sur le HIV qui apparement ne veulent pas trouver de remède simple et direct à la maladie (les branleurs quand même!!)...

              Malheusement les chercheurs , ces nantis, n'ont pas le pouvoir des taxis en France...
          • [^] # Re: Et après ça ..

            Posté par . Évalué à 4.

            Je suis dans la même situation que toi et j’ai une impression similaire concernant le retour en France. Beaucoup de gens que connais veulent revenir pour des raisons sentimentales (famille, amis). Pas mal préfèrent arrêter la recherche pour revenir en France s’il n’y trouvent pas de poste permanent, alors qu’ils aurait pu continuer à l’étranger. En revanche les conditions de recherche jouent contre la France. Quand on voit les moyens absolument ridicules en France et les efforts qu’il faut produire pour obtenir de l’argent. Aux USA ils passent aussi pas mal de temps pour avoir des bourses mais au final pour le même effort ils reçoivent 20 fois plus de pognon. Au final le « Brain drain » est assez faible en France. Rien à voir avec ce qu’il se passe en Italie par exemple. À la louche dans mon domaine je dois connaître environ 10 italiens en poste à l’étranger (France et USA principalement) pour chaque italien travaillant en Italie.

            Pour ma part je suis fraîchement expatrié donc il est difficile de savoir ce que je vais faire. Je suis attaché à mon pays mais je n’ai pas forcément pour objectif de revenir en France. Après si je trouve une fille ici, je sens que ça va encore diminuer ma motivation. :)
            • [^] # Re: Et après ça ..

              Posté par . Évalué à 5.

              Après si je trouve une fille ici, je sens que ça va encore diminuer ma motivation.

              Ce peut avoir un effet contraire. Avant j'etais 50/50 sur rester ou revenir en France. Lorsque j'ai trouve "une fille ici", je pensais que ca diminuerai ma motivation pour revenir. Neni! Elle veut venir en France....
    • [^] # Re: Et après ça ..

      Posté par (page perso) . Évalué à 7.

      Le problème c'est que la recherche française, il n'y a pas de telle chose. Joseph Sifakis est né si mes souvenir son bon en crète ;-) La recherche a quasi toujours été internationnale. On travaille toujours sur les briques que d'autres ont posées.

      Les professeurs universitaires ont, par ailleurs, toujours été d'origines diverses et ceci dans tous les pays.
      • [^] # Re: Et après ça ..

        Posté par . Évalué à 3.

        La recherche est internationale, mais le context local se ressent dans l'ecriture des articles de recherche. Je n'ai pas pour habiture de lire les auteurs d'un papier avant de lire le contenu. Cependant, il m'arrive en lisant le contenu de dire "tient ca c'est francais" et immanquablement, et regardant l'origine des auteurs (le centre de recherche ou universite, pas l'origine de l'auteur en lui-meme) je me surprend en etant dans le vrai.

        Un mot clef qui est souvent discriminateur: "meta". Si "meta" est utilise plus d'une fois dans le resume ou l'introduction de l'article, c'est imparable.... C'est francais. [l'alternative "abstraction" semblerai etre adopte par les autres]. Je suggererai meme a quelqu'un de faire une these sur l'identification de mot-clefs et leur association avec l'origine de l'article...
        • [^] # Re: Et après ça ..

          Posté par . Évalué à 2.

          Quand il y a écrit "meta" à tous les paragraphes mais que ça résout des problèmes déjà traités il y a vingt ans. Que ça n'a jamais lu l'état de l'art (écrit en anglais, quelle horreur) et que ça parle avec l'accent franchouillard le plus imbitable possible en conf., c'est à coup sûr Français. :-)
    • [^] # Re: Et après ça ..

      Posté par . Évalué à 4.

      Ces recherches dates de 1980....alors peut être que c'est en 1980 que la recherche se portait bien en france. De manière général les grandes distinctions (nobel, turing, ...) viennent couronner une carriére et récompense des travaux anciens; probablement pour être sur de ne pas céder à un effet de mode et récompenser un travail qui au final n'a rien de bien novateur.

      Etant par ailleurs moi même dans ce monde de la recherche je peux te dire que les vieux ils disent vous êtes dans la merde désolé. Les jeunes ils cherchent a survivre et trouver un financement pour mener leurs recherches mais c'est souvent décourageant, Naturellement comme dans toute profession il y a aussi des planqués qui pensent qu'a leur carriére, ou ceux qui ont chopé un obscur poste et qui se la coule douce. Je pense qu'au finale il s'agit d'un bon échantillons de la société francaise: certains qui profitent grâce à une grande majorité qui est payé au lance pierre.

      Allez je retourne broyer du noir dans ma cage...
      • [^] # Re: Et après ça ..

        Posté par . Évalué à 2.

        Oui enfin les « vieux » ont vécu une époque dorée aussi. Je connais des chercheurs qui à l’époque ont eu un poste permanent une fois la maîtrise en poche, on leur demandait juste de faire une thèse après quelques années quand même. Je connais quelques post-docs qui ont eu du mal à avaler qu’aux concours ces mêmes personnes leur expliquent que non, 4 ans de postdoc ce n’est pas assez. Les mêmes qui d’ailleurs restent dans les labos après 65 ans ce qui bloque la création d’un poste correspondant pour les jeunes (nouvelle règle du ministère, résultat par rapport à l’année dernière dans mon domaine le nombre de postes ouverts passe de 9 ou 10 à 3 pour un concours, toujours avec 150 candidats bien sûr).
      • [^] # Re: Et après ça ..

        Posté par . Évalué à 9.

        La quantité de planqués dépend énormément du système. Le système universitaire francais à tendance à transformer en planqués des gens motivés au départ. Attention je ne dis pas qu'au final ils sont une majorité, mais ils sont clairement plus nombreux qu'ils devraient être.

        Beaucoup de jeunes chercheurs recrutés comme permanents sont lachés dans d'obscurs labos, trop petits, ou l'activité de recherche est souvent faible. Et comme on manque d'enseignants, on les pousse à faire un max d'heures sup. Eux ils acceptent (les pressions sont souvent importantes, et puis c'est vrai que 700 euros par mois quand on en gagne 1800, ce n'est pas rien), et bien sur ils n'ont plus le temps de faire de la recherche, et décrochent. Il faut s'imaginer ce que c'est pour un chercheur d'essayer de se motiver quand il est déja débordé, seul, qu'il n'y a personne autour de lui pour s'intéresser à ses travaux, et que de toute facon tout le monde se fout de savoir si il fait de la recherche ou pas.

        Après, au bout de 4 ou 5 ans, ils commencent à souffler un peu au niveau enseignement (moins de préparation nécessaire), mais pour reprendre le train en marche, c'est pas gagné...

        Voila, c'est un peu hors sujet, mais je crois que la plupart des gens hors du système ont une vision trop tranchée et caricaturale de ce qu'est un planqué / non planqué à l'université. C'était juste pour montrer que les choses ne sont pas simples.
        • [^] # Re: Et après ça ..

          Posté par (page perso) . Évalué à 1.

          C'est tellement vrai ce que tu racontes...
          Personnellement j'étais parti pour candidater sur des postes de MCF cette année, et vu comment se déroule cette année, j'ai de moins en moins envie... 3/4 enseignement pour 1/4 recherche (ATER temps complet), c'est vraiment dur de se motiver après la thèse !

          Et je sais que si je passe MCF, ce sera comme ça, voire pire, pendant 3 ou 4 ans. Largement de quoi décrocher, comme la grosse majorité de MCFs que je connais qui au mieux ne font que de l'encadrement en recherche (et de façon plus ou moins heureuse...) . Faut pas se leurrer, le statut de MCF c'est avant tout de l'enseignement... Ou alors il faut bosser 12H par jour 7j/7, ce qui n'est pour moi pas acceptable avec un salaire aussi minable.
  • # cursus de base ?

    Posté par (page perso) . É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.
    • [^] # Re: cursus de base ?

      Posté par . Évalué à 5.

      j'ai étudié tout ça "théorie des automates, logique temporelle, probabilités (chaînes de Markov et compagnie)..." en master 1 et 2
      mais le model checking ça m'évoque rien comme ça, et puis j'ai l'impression d'avoir quasiment tout oublié pourtant ça fait que 2 ans et demi ...

      la logique temporelle c'est vraiment un bon morceau, c'est pas complexe en soit mais la gymanistique du cerveau et de projection dans le temps est assez éprouvante.
    • [^] # Re: cursus de base ?

      Posté par . Évalué à 6.

      Chaînes de Markov, réseaux neuronaux.... Miam, ça me rappelle l'époque étudiante où on avait des cours intéressants, on foutait rien à côté, et on arrivait à s'en plaindre.
      • [^] # Re: cursus de base ?

        Posté par . Évalué à 6.

        Pareil, sauf que je bossais énormément, et que je me plaignais un peu les semaines de 60h de boulot.

        Qu'est ce qu'on est tranquille quand on travaille ;)
  • # Le libre c'est aussi...

    Posté par (page perso) . É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...

Suivre le flux des commentaires

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