au sommaire
Joseph Sifakis. Crédit : Photothèque CNRS Bellevue
Rappelons que le panthéon de l'informatique est dominé par deux dieux à qui l'on doit les bases théoriques de l'informatique et les premières réalisations d'ordinateurs. Le premier est le mathématicienmathématicien d'origine hongroise John Von NeumannJohn Von Neumann, dont les contributions phénoménales à la science du XXième siècle sont nombreuses. En particulier, son nom est associé aussi bien aux fondements des mathématiques qu'à ceux de la mécanique quantiquemécanique quantique. C'est aussi lui qui a introduit les automates cellulaires et à qui l'on doit ce qu'on appelle l'architecture de Von Neumann utilisée dans la quasi totalité des ordinateurs modernes.
John Von Neumann et Robert Oppenheimer deavnt un des premiers ordinateurs à Princeton.
Crédit : IAS Princeton University
La seconde divinité, à qui la première doit vraisemblablement une partie non négligeable de son inspiration (sans doute lorsque les deux ont discuté ensemble à Princeton à la fin des années 1930) est le mathématicien anglais Alan TuringAlan Turing. Comme Von Neumann, Turing était un enfant prodige mais c'était aussi un sportif de haut niveau qui aurait pu être sélectionné pour l'épreuve du marathon aux Jeux olympiques.
On lui doit entre autre la fameuse machine de Turing (à la base de la théorie des ordinateurs), le fameux test de Turing (pour déterminer si la conscience peut être simulée par un ordinateur) et des travaux en avance sur son temps sur la modélisationmodélisation mathématique de la morphogenèsemorphogenèse avec ce qui est aujourd'hui connu sous le nom de structure de Turing.
Tout comme les travaux de Von Neuman portant sur la mise au point de la bombe A, les siens, en cryptologie, ont changé le cours de l'histoire, car il est connu pour avoir cassé le code de chiffrage des messages secrets allemands pendant la guerre.
Alan Turing (1912-1954)
C'est donc en son honneur que chaque année depuis 1966 l'Association for Computing Machinery (ACM) décerne un prix d'une valeur de 250.000 dollars.
Joseph Sifakis s'est vu décerner le 4 février 2008, avec Edmund Clarke (Carnegie Mellon University) et Allen Emerson (Université du Texas, Austin), le prix Turing 2007.
L'ACM, fondée en 1947, est l'organisation internationale représentative des informaticiens avec pour mission la diffusiondiffusion des résultats de la recherche par l'édition de journaux et l'organisation de conférences. C'est la première fois que ce prix prestigieux, équivalent du prix Nobel pour les informaticiens, est décerné à un chercheur français.
Comment vérifier un programme, un matériel, une organisation ?
Joseph Sifakis est actuellement directeur de recherche (CNRS) au laboratoire Verimag à Grenoble dont il est le fondateur. A l'origine ingénieur électricien de l'Ecole Polytechnique d'Athènes et maintenant docteur d'Etat en Informatique de l'Université de Grenoble, il est reconnu pour ses travaux innovants sur des aspects aussi bien théoriques que pratiques de la modélisation et de la vérification des systèmes temps réel.
Il est justement, avec Edmund Clarke et Allen Emerson, l'un des pères fondateurs de la méthode algorithmique connue sous le nom de Model Checking et ce sont ces travaux que le prix Turing vient récompenser.
Cette méthode algorithmique permet de vérifier qu'un système logiciel ou matériel satisfait à des exigences données. Elle trouve de nombreuses applicationsapplications industrielles avec la vérification des puces, des protocoles de communication, des logiciels pilotes de périphériques, des systèmes critiques embarqués (par exemple dans les avions, les trains, les fuséesfusées, les satellites ou les téléphones portables...) et des algorithmes de sécurité. Tous systèmes qui exigent donc une extrême fiabilité.