Présentation des travaux du Centre de Recherche Commun
Introduction, par Jean-Jacques Lévy, Directeur du Centre de Recherche Commun INRIA – Microsoft Research
Jean-Jacques Lévy a proposé un aperçu du nouveau laboratoire et de son organisation. Ce sont douze chercheurs qui sont montés à bord en 2006, à terme ils seront 30. Les deux axes de recherche du nouveau laboratoire peuvent se résumer d’une part en « méthodes formelles et sécurité du logiciel », et « Interaction avec les données scientifiques », d’autre part, ce que les scientifiques du centre commun ont pour habitude de nommer « track A » et « track B ». Trois projets sont d’ores et déjà en cours pour le track A. En ce qui concerne le track B, deux projets sont en préparation et deux en prévision. Tous les projets sont réalisés par une équipe mixte, composée à la fois de chercheurs de l’INRIA et de chercheurs de Microsoft Research.
Télécharger la présentation de Jean-Jacques Lévy, Directeur du Centre de Recherche Commun INRIA – Microsoft Research
(.pps | 4,17 Mo)
Track A : méthodes formelles et sécurité du logiciel
| • |
Le premier projet s'intitule « Composants mathématiques ». Ici l’équipe s’intéresse à l’utilisation d’outils informatiques pour réaliser de très longues preuves de démonstrations mathématiques. En application de ses outils, Le projet s’intéresse à des théorèmes ou problèmes célèbres dont la démonstration n’a pu être prouvée : par exemple le théorème des quatre couleurs, le problème de classification de Feit-Thompson ou la conjecture de Kepler. | | • |
Le deuxième projet s’intitule « Outils et méthodologies pour les spécifications formelles et les preuves ». Ce projet est basé sur TLA+, langage de spécification de preuves proposé par Leslie Lamport. Il a trait aux preuves naturelles avec la théorie des ensembles et utilise la logique temporelle des actions. | | • |
Le troisième projet s’intitule « Calculs sécurisés distribués et preuves formelles ». Son objectif vise à garantir la communication sécurisée sur les réseaux, en développant des langages de programmation qui incluent des primitives de sécurité et des techniques formelles permettant de prouver la sécurité des programmes distribués. |
Composants mathématiques Dans son introduction, Georges Gonthier a présenté son approche qui vise à formaliser la partie mathématique d’une preuve, en s’appuyant sur le système Coq pour vérifier automatiquement l’absence d’erreur. Une partie de la genèse du projet est liée au théorème des quatre couleurs, resté incomplètement démontré durant près de 150 ans.
Georges Gonthier, en collaboration avec Benjamin Werner, a complètement vérifié sa démonstration en utilisant le système Coq, mis au point à l’INRIA. Quel est l’intérêt de cette démonstration? Elle a permis peut-être de construire des outils qui pourront être réutilisés pour verifier et corriger des programmes. 
Télécharger la présentation de Georges Gonthier
(.pps | 1,95 Mo)
Track B : interaction avec les données scientifiques
| • | Le premier projet de cet axe de recherche s’intitule ReActivity et vise à proposer à la communauté scientifique au sens large des outils pour permettre aux scientifiques d’interagir avec les immenses flots de données issus de leurs expérimentations. | | • | Ce sont quatre projets au total qui devraient être lancés dans cet axe de recherche, les trois suivants sont actuellement au stade de la définition. |
ReActivity
Les quantités de données traitées sont de plus en plus complexes, et les utilisateurs de plus en plus exigeants. Pour essayer de comprendre les problématiques et parce que les problèmes rencontrés par les scientifiques sont les mêmes que dans la vie de tous les jours, Wendy MacKay et ses équipes sont allés observer sur le terrain, dans leurs laboratoires, des scientifiques, des biologistes, des historiens, des artistes, des informaticiens. Ils en ont tiré des conclusions, par exemple que les biologistes ont besoin d’une plus grande flexibilité entre l’instrument et l’être humain. Ou que pour les historiens, l’essentiel est l’endroit où se trouvent les données, et que ces données ne soient surtout pas perdues.
Les objectifs dans ce projet sont de créer :
| • | des technologies pour garder les liens entre le monde physique et le monde en ligne | | • | des outils pour réagir face à des données temporelles multi-échelles complexes | | • | des plateformes de données communes pour échanger des données dans des environnements différents | | • | des technologies innovantes pour transformer les données. |
Télécharger la présentation de Wendy MacKay, Chercheur
(.pps | 17,4 Mo)
|
|
