Inscrivez-vous gratuitement à la Newsletter BFM Business
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 Sophia-Antipolis.a.muller@01informatique.presse.fr
Votre opinion