Directeur de recherche au CNRS |
---|
Naissance | |
---|---|
Nom dans la langue maternelle |
Ιωσήφ Σηφάκης |
Nationalités | |
Formation | |
Activités |
A travaillé pour | |
---|---|
Membre de | |
Directeurs de thèse |
Jean Kuntzmann (), Louis Bolliet (d) |
Site web | |
Distinctions |
Joseph Sifakis (en grec moderne : Ιωσήφ Σηφάκης, Iosif Sifakis) est un chercheur en informatique français d'origine grecque[1], né le à Héraklion (Crète), directeur de recherche au CNRS et membre de l'Académie des technologies.
En 2007, il est le premier lauréat français à recevoir le prix Turing. Ce prix, considéré comme l'équivalent du prix Nobel, est la plus haute distinction en informatique.
Ses travaux de recherche portent principalement sur les systèmes embarqués critiques[2] (nucléaire et transport).
Joseph Sifakis est ingénieur électricien de l’École polytechnique d’Athènes, docteur-ingénieur de l'université Joseph-Fourier (USMG)[3]. En 1970, il arrive en France pour y poursuivre une thèse en physique théorique mais rapidement s'intéresse à l'informatique. Il devient docteur d’État en informatique de l'USMG et de l'Institut polytechnique de Grenoble[4].
Il est directeur de recherche de classe exceptionnelle (depuis 2011, émérite) au CNRS et fondateur du laboratoire Verimag[5] près de Grenoble (unité mixte de recherche du CNRS, de l'université Joseph-Fourier et de Grenoble INP), où il travaille encore à présent.
En 2007, il reçoit le prix Turing[6], avec Edmund Clarke (Carnegie Mellon University) et Allen Emerson (université du Texas à Austin) pour la méthode d'énumération et de vérification de modèles (model checking). Cette méthode se fonde sur une description des systèmes informatiques par des systèmes à états et transitions et sur une analyse des états accessibles dans ces systèmes, qui s'inspire des algorithmes de parcours de graphes[7].
Son application permet de vérifier qu'un système représenté par un modèle formel satisfait des propriétés formulées dans une logique temporelle. Cette méthode est particulièrement adaptée sur des propriétés essentielles du comportement du système en fournissant la preuve formelle qu'un système est "correct" (contrairement à des méthodes de validation ad hoc fondées sur le test)[8].
De ce fait, le model checking est particulièrement adapté pour assurer des propriétés de sûreté et par conséquent transposable à de nombreuses applications industrielles : puces, protocoles de communication, logiciels pilotes de périphériques, systèmes critiques embarqués (par exemple dans les avions, les trains, les fusées, les satellites ou les téléphones portables…) et d’algorithmes de sécurité.[9]
Les récipiendaires se partagent une prime de 250 000 dollars[10].
Il s'est également illustré dans l'étude des systèmes hybrides.
En 2001, il reçoit la médaille d'argent du CNRS[11]
En 2009, il devient docteur honoris causa de l'École polytechnique fédérale de Lausanne, où il devient professeur ordinaire, pendant la période 2011–2016, dirigeant le Laboratoire pour la conception rigoureuse des systèmes[12].
Il est élevé à la dignité de Grand officier de l'ordre national du Mérite [13]. Il est nommé au grade de Commandeur de la Légion d'honneur le [14].
En 2024, il est élu membre de l'Académie nationale des sciences (États-Unis)[15].
Joseph Sifakis a activement travaillé pour le transfert des résultats de la recherche vers des partenaires industriels. De 2004 à 2011, il est le coordinateur scientifique du réseau d’excellence européen « ARTIST2 Embedded Systems Design » qui coordonne la recherche de 35 équipes européennes afin de développer des résultats théoriques et pratiques pour la conception de systèmes embarqués performants et robustes [16].