Sites Inria

English version

European Research Council 2011

Sophy Caulier - 6/12/2011

Dale Miller : Faire que la preuve soit universelle

© Inria / Photo Kaksonen

Bénéficiaire d’une bourse ERC Advanced Grant destinée aux chercheurs confirmés, Dale Miller s’engage sur le difficile chemin de la preuve. Son objectif : dans ce domaine très abstrait mais qui a un impact certain sur le monde réel, standardiser les systèmes de preuve et leur délivrer des certificats afin d’améliorer la confiance que l’on peut avoir en eux.

Dale Miller en est convaincu : l’obtention du financement ERC va les aider lui et Parsifal, son équipe-projet, à avancer de façon significative sur le long chemin de la preuve. Et cette avancée bénéficiera à tout le monde ! Cette preuve est un peu le Graal des chercheurs en sciences informatiques et mathématiques. Comment prouver qu’un logiciel ou un circuit électronique fait bien ce qui est attendu de lui et qu’il le fait dans les conditions et conformément aux spécifications qui ont présidé à sa création ? Pour prouver la validité d’un programme de plusieurs millions de lignes de code, il faut parfois concevoir un nouveau programme, composé lui de plusieurs centaines de milliers de lignes de code…

Le sujet est loin d’être trivial. Les systèmes numériques se multiplient et pas seulement dans les domaines des loisirs ou du divertissement, domaines dans lesquels l’utilisateur peut relancer lui-même son système en cas d’erreur ou se passer d’une fonction si elle est affectée par un bug . Aujourd’hui, des codes et des programmes pilotent, contrôlent, automatisent de nombreuses tâches qui ont un impact sur nos vies quotidiennes et qui ne tolèrent aucun dysfonctionnement. Le lancement d’une fusée  qui va larguer un satellite de communications supposé fonctionner de façon autonome pendant une quinzaine d’années doit être fiabilisé à 100%. De même, le monitoring de la température d’une couveuse  ou du rythme cardiaque d’un patient qui vient d’être opéré du cœur ne supporte aucune défaillance. Sans parler des avions de ligne, des systèmes de transactions bancaires, des télécommunications, etc. À cela s’ajoute la question de la sécurité, c’est-à-dire comment protéger tous ces objets numériques des virus et des attaques malveillantes.

Dale Miller travaille sur ces sujets depuis longtemps. Après un Ph.D. en mathématiques à l’université de Carnegie Mellon, il est professeur et chercheur en informatique. D’abord aux États-Unis, puis en Europe où sa matière, la logique computationnelle, bénéficie d’un grand intérêt des milieux de la recherche. Edimbourg, Glasgow, Gênes, Pise, Sienne l’attirent tout particulièrement. Mais c’est en France qu’il trouve son centre de gravité. Cet Américain marié à une Italienne, s’installe en région parisienne en 2002 lorsqu’il devient directeur de recherche au centre Inria de Saclay et professeur à l’École polytechnique. Son français n’est pas à la hauteur de son investissement dans la recherche hexagonale, « il faudrait que je quitte le labo si je voulais vraiment parler français !  », affirme-t-il. C’est vrai qu’il est quotidiennement entouré d'une équipe cosmopolite : un Allemand, un Américain, un Indonésien, des Néerlandais, des Italiens... et quelques Français. Et que la langue de travail dans la recherche reste l’anglais !

L’idée est de créer une place de marché où il sera possible d’échanger et de partager les systèmes de preuve élaborés ici ou là.

Il invoque la Tour de Babel, non pour parler du multilinguisme de son environnement, mais bien pour décrire la situation en matière de preuve. « Il n’existe aucun standard dans ce domaine. Chaque fois qu’il faut prouver qu’un système fonctionne, il faut un budget et un étudiant pour développer un vérificateur des preuves de propriétés du système. Et encore, ce vérificateur est conçu ad hoc et il ne fonctionne que pour un seul système. Parfois, il ne marche même pas pour la version suivante du système !  ». Le contre-exemple le plus explicite est celui des fichiers texte : « depuis que quelqu’un a inventé le langage html, les fichiers peuvent être lus par n’importe quel navigateur. C’est ce à quoi nous voulons parvenir dans le domaine de la preuve. ».

Son idée : faire de la « chimie informatique  », c’est-à-dire utiliser les atomes d’inférences existants pour élaborer des molécules d’inférences. Autrement dit, proposer des modules de systèmes de preuves certifiés pour pouvoir composer un système arbitraire… « L’idée est de créer une place de marché où il sera possible d’échanger et de partager les systèmes de preuve élaborés ici ou là  ». Pour parvenir à cela, Dale Miller envisage de délivrer des « certificats de preuve », c’est l’objet du projet ProofCert qui lui a valu la bourse ERC. « En fait, ce sujet est très abstrait, mais il a un vrai impact sur le monde réel et sur notre vie...  », conclut-il.

ProofCert, certifier la preuve !

Pendant trois années, Dale Miller a peaufiné le projet ProofCert dans différents colloques et auprès d’agences de financement avant de se voir attribuer la bourse ERC Advanced Grant, soit 2,2 millions d’euros pour cinq ans à compter de janvier 2012. Concrètement cela va se traduire par le recrutement de doctorants, de postdoctorants et d'invitations de nombreux chercheurs du domaine.

Très schématiquement, l’objectif de ProofCert est de standardiser les systèmes de preuve, de les certifier, de les répertorier dans une bibliothèque et de les mettre à disposition sur une place de marché. « L’idée est d’instaurer une confiance dans les systèmes de preuve existants afin que les gens puissent échanger et partager leurs travaux dans ces domaines  », explique Dale Miller, « un peu comme dans le domaine des virus et des antivirus, qui est aujourd’hui très dynamique et très coopératif  ».

Lauréats 2011

Dans la catégorie "Jeunes chercheurs", Remi Gribonval  (Metiss, Rennes), Andreas Enge  (Lfant, Bordeaux), Xavier Rival  (Abstraction, Rocquencourt), Erwan Faou  (Ipso, Rennes) ont reçu une bourse qui leur permettra de constituer une équipe. Dans la catégorie "chercheurs confirmés", ce sont les projets de Marie-Paule Cani (Evasion, Grenoble), Nicholas Ayache (Asclepios, Sophia Antipolis)  et Dale Miller (Parsifal, Saclay), qui ont été retenus par l'ERC.

Mots-clés : Equipe-projet Parsifal Inria Saclay Ile-de-France ProofCert Preuve de programmes Systèmes de preuves Standards Certificats Dale Miller

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !