Inria-Microsoft : la preuve que ça marche

Des logiciels plus fiables. C'est l'un des enjeux des travaux sur la preuve formelle, menés par le laboratoire commun à Microsoft et à l'Inria.

Preuves formelles d'un côté, ingénierie scientifique de l'autre. Les deux grands axes de recherche du laboratoire commun à l'Inria (Institut national de recherche en informatique et en automatique) et à Microsoft ont été fixés par un comité scientifique, coprésidé par Michel Cosnard, président de l'institut, et Andrew Herbert, directeur du laboratoire de Cambridge Microsoft Research. Parité oblige, chaque projet doit réunir des chercheurs des deux structures. Installé à Orsay, en région parisienne, ce laboratoire devrait, à terme, rassembler une trentaine de chercheurs. Parmi les douze qui l'ont déjà rejoint, le plus célèbre est certainement Leslie Lamport, du centre de Palo Alto de Microsoft Research. Inventeur du langage de spécification TLA (logique temporelle d'action), il travaille au laboratoire commun sur l'algorithmique répartie. D'abord chez Digital, puis chez Compaq à partir de 1985, et enfin chez Microsoft Research depuis 2001, Leslie Lamport a toujours été un chercheur. Sa démarche, fondée sur les affinités scientifiques, illustre bien le mode de fonctionnement du laboratoire. Embarqué sur un projet de deux ans, il sera physiquement présent à Orsay entre trois et quatre mois par an. En terrain connu. ' J'étais déjà en relation avec des chercheurs de l'Inria, dit-il. Damien Doligez et Stéphane Merz ont été respectivement stagiaire et post-doc chez Digital. ' Tous deux chercheurs à l'Inria, le premier travaille sur la démonstration formelle, et le second sur la qualité et la sûreté des logiciels.

Des modèles pour la tolérance de pannes

Construire des systèmes qui marchent, même si un ou plusieurs ordinateurs tombent en panne. Telle est l'ambition de Leslie Lamport. ' Les algorithmes répartis relèvent de problématiques de synchronisation des processus, explique-t-il. La question est de savoir comment séparer des processus, qu'ils soient dans un même ordinateur ou répartis sur un réseau. ' L'enjeu scientifique ? ' Je cherche depuis longtemps un modèle capable de vérifier les preuves d'un système. ' Pas de résultats tangibles attendus sur ce projet avant deux ou trois ans. Pire : ' Il faudra bien compter encore dix ou vingt ans avant que l'on utilise les preuves dans les ordinateurs ordinaires ', précise Leslie Lamport. La difficulté ? ' Nous ne savons toujours pas déterminer à l'avance si un modèle, celui d'un avion par exemple, sera bon. En revanche, nous savons que si le modèle comporte une erreur, il y aura un problème dans l'avion. C'est la même chose dans les ordinateurs. '

L'alliance des maths et de l'informatique

Georges Gonthier, Cédric Fournet... Les noms des chercheurs de Microsoft Research qui travaillent au centre de recherche commun sur la preuve formelle ont souvent une consonance française. Rien d'étonnant à cela : le laboratoire a été constitué sur la base des travaux scientifiques se rapportant aux preuves formelles. Et les Français excellent en la matière. ' Je suis chercheur au laboratoire de Cambridge de Microsoft Research depuis trois ans, explique Georges Gonthier. Auparavant à l'Inria, j'ai gardé au travers de mes recherches beaucoup de liens avec mes anciens collègues. ' Le laboratoire commun a été l'occasion d'officialiser ces collaborations. Et de poursuivre un vieux rêve. Georges Gonthier avait déjà travaillé à l'Inria sur le théorème des quatre couleurs, et prouvé qu'il est possible de colorier une carte avec quatre couleurs sans que jamais deux régions d'une même couleur ne se touchent (voir encadré p. 38). Nouvelle façon de faire des maths autant que nouvelle manière d'envisager l'informatique, le projet de Georges Gonthier consiste à utiliser les mathématiques pour établir la preuve formelle en informatique. ' Mon objectif est de comprendre quelle doit être l'ingénierie de la preuve formelle, explique-t-il. Dans l'informatique, nous commençons à peine à maîtriser les éléments sources des programmes. Nous en sommes tout juste à vérifier que les opérations élémentaires s'effectuent correctement, pas encore à voir si l'ensemble marche bien. Or, c'est cela que je veux explorer grâce aux mathématiques qui s'inscrivent dans un cadre formel. ' Ce projet fait suite aux travaux menés à l'Inria sur l'analyse de programmes réels, notamment les logiciels de vol d'Ariane. Puis aux rencontres avec des collègues de Sophia-Antipolis autour de discussions scientifiques, de définitions d'hypothèses, de directions de recherche. ' Nous avons démarré ce travail il y a quatre mois, poursuit Georges Gonthier. Mais nous ne voulons pas que le laboratoire commun reste isolé de la recherche de Microsoft. C'est pourquoi nous essayons de faire venir des chercheurs ici. '

Les premiers pas de l'ingénierie scientifique

' Nous avons eu du mal à trouver cette appellation d'ingénierie scientifique ', avoue Jean-Jacques Levy, directeur du laboratoire commun. Il s'agit de développer des logiciels utiles aux scientifiques, comme Latex, le langage de composition des textes scientifiques inventé par Leslie Lamport. Concernant ce deuxième grand domaine d'investigation du laboratoire, quatre projets sont actuellement en lice. Le plus avancé, celui de Bruno Salvy, champion du calcul formel, vient tout juste d'être accepté. ' Son objectif est de bâtir une encyclopédie dynamique des mathématiques ', précise Jean-Jacques Levy. A l'image des bréviaires auxquels se référent les scientifiques chaque fois qu'ils ont une équation à résoudre, mais en tirant profit d'internet, comme le fait Wikipedia.Le deuxième projet, encore en évaluation, est celui de Wendy MacKay, directrice de recherche au sein d'Inria Futurs. Il consiste à créer un workflow de travail collaboratif pour les scientifiques afin de réunir leurs ' cahiers d'expérience '. Très ambitieux, il a vocation à tracer toutes les découvertes scientifiques. La difficulté réside dans le nombre phénoménal de problèmes rencontrés dans une recherche.Les deux autres projets pressentis portent l'un sur l'analyse vidéo, et l'autre sur l'analyse des données. Le premier est mené par Patrick Pérez, de l'Inria de Rennes. Son but est de repérer des objets précis dans des images tirées d'une vidéo. Le second est un projet relatif à l'utilisation des méthodes géométriques pour l'analyse des données, déjà en cours à l'Inria de [e-mail]

Les points clés de la collaboration

Février 2005 : naissance d'un projet de laboratoire commun entre Microsoft et l'Inria.
Avril 2005 : signature du mémorandum par Gilles Kahn, président de l'Inria, et Steve Ballmer, PDG de Microsoft.
Mai 2006 : désignation des premiers chercheurs.

10 millions d'euros, financés à parts égales par l'Inria et Microsoft. Première mondiale pour l'éditeur, qui noue un partenariat avec un centre de recherche public.

30chercheurs prévus à terme, 12 actuellement.
3 projets retenus, 4 en cours d'évaluation.

Michel Cosnard (Inria) : ' nous partageons une vraie cohérence de vue avec Microsoft '

Le laboratoire commun s'inscrit-il dans la stratégie de l'Inria ?
Michel Cosnard : Parmi les sept thèmes du plan stratégique de l'institut pour les années 2008 à 2013, deux d'entre eux concernent directement le laboratoire commun. A savoir le futur de la programmation sous l'angle de la sécurité et de la qualité, et l'utilisation des technologies de l'information dans les différentes disciplines scientifiques.

Comment les chercheurs du laboratoire commun ont-ils été choisis ?
M.C. : Le scénario s'est déroulé en plusieurs étapes. Il y a d'abord eu la définition des différents domaines de recherche communs entre l'Inria et Microsoft Research. Nous avons ensuite, dès la fin 2005, lancé un appel au volontariat au sein de l'Inria en tenant compte des affinités entre les personnes. Une démarche identique est en cours aujourd'hui sur les autres projets.

Quelle est votre politique en matière de propriété intellectuelle ?
M.C. : L'exploitation des droits de propriété se fait au cas par cas. Mais cela ne m'inquiète pas, car, à l'Inria, nous avons déjà une grande pratique de la propriété intellectuelle.

Le théorème des quatre couleurs

L'ordinateur apporte du neuf aux mathématiques, mais l'histoire n'est pas nouvelle : le casse-tête des quatre couleurs débute en 1852, avec Francis Guthrie. Ce cartographe anglais remarque que quatre couleurs suffisent pour peindre la carte des cantons d'Angleterre sans qu'aucun canton adjacent ait la même teinte. Il demande alors à son frère mathématicien si cette propriété est applicable à toutes les cartes. Le problème est publié à l'Académie royale en 1879. Personne ne le résout jusqu'en 1976, où une première solution est proposée : Appel et Haken réalisent le programme de Heesch à l'aide de dizaines de milliers de figures... et 1 200 heures de calcul. Difficile à vérifier. En 1995, quatre mathématiciens simplifient les calculs grâce à des ordinateurs plus puissants. Mais ils utilisent le langage C, pas assez ' mathématique '. Dix ans plus tard, Georges Gonthier et Benjamin Werner valident la preuve en utilisant le langage Coq de l'Inria, qui vérifie la démonstration étape par étape.

3 questions à... : Jean-Jacques Levy, directeur du centre de recherche commun Inria-Microsoft Research, basé à Orsay

Quelles sont les applications des recherches que vous effectuez ?
' Une preuve est une spécification écrite dans un langage formel, qui détaille les étapes élémentaires de la logique. Appliquées à l'informatique, ces méthodes formelles devraient donc nous indiquer comment améliorer la qualité des logiciels. Mais les preuves dans le logiciel étant de ' longues preuves ', nous nous faisons la main sur des problèmes mathématiques aux buts précis, comme la théorie des quatre couleurs. '

Vos résultats sont-ils facilement transposables ?
' Nous faisons de la recherche à long terme, mais elle intéresse les entreprises. Certains de nos logiciels sont ainsi en fonction sur la ligne 14 du métro parisien. Ce qui prouve bien que nous conservons des facultés de praticiens même dans nos activités les plus fondamentales. C'est un atout des théoriciens français. Ils savent allier théorie et pratique parce qu'ils ont une forte culture mathématique. Et c'est pourquoi nos travaux arrivent souvent assez rapidement sur le marché. '

Vos recherches sont-elles publiques ?
' Relevant de la recherche fondamentale, les logiciels mis au point dans le cadre du laboratoire seront publics et disponibles sous la licence libre Cecill B. Nous la préférons à GPL, plus contraignante, car si un bout de logiciel l'adopte, cest tout le logiciel qui passe en GPL. '