Le prestigieux Turing Award, tiré du nom d’Alan Turing, père fondateur de l'Informatique, récompense chaque année une personne sélectionnée pour sa contribution technique faite à la communauté informatique. « Les contributions doivent être d’une importance durable et majeure dans le secteur informatique » conditionne la page officielle de l’Association for Computing Machinery (ACM). Un prix de 250 000 dollars récompense l’heureux élu, financée par Intel et Google.

Cette année c’est Joseph Sifakis, un directeur de recherche au CNRS, laboratoire VERIMAG (CNRS/Université Grenoble 1/Groupe Grenoble INP) qui reçoit ce « prix Nobel » de l’informatique, avec deux autres de ses confrères américains (Edmund Clarke et Allen Emerson).

Cette équipe est connue pour avoir mis au point le Model Checking, méthode algorithmique de vérification des systèmes complexes, réputée performante et fiable, et « aujourd'hui très largement utilisée dans les industries du logiciel et du matériel » explique le CNRS. Cette méthode permet en pratique de vérifier qu’un système logiciel ou matériel satisfait à des exigences données (de sécurité ou de sûreté par exemple). Du coup, elle est suivie à peu près partout : puces, protocoles de communication, logiciels pilotes de périphériques, systèmes critiques embarqués, etc.

« Les travaux de Joseph Sifakis sont déterminants et ont conduit à la création de nouvelles logiques de spécification, à de nouveaux algorithmes de vérification et à des résultats théoriques exceptionnels, rajoute le CNRS, alors que cette technologie est aujourd’hui utilisée dans l’industrie des circuits intégrés afin de concevoir des systèmes complexes dont on peut garantir la conformité aux spécifications initiales »

L’impact industriel du Model Checking devrait être encore plus significatif dans les années à venir notamment en ce qui concerne la vérification des processeurs et des systèmes critiques embarqués.