Les recherches du Centre de Recherche Commun INRIA – Microsoft
Research s'articulent autour de deux axes de recherche : les
méthodes formelles et les outils informatiques pour
les Sciences.
Sur l’axe de recherche lié aux méthodes formelles, 3 projets ont
démarré en 2006.
L’objectif est de contribuer à faire progresser les
langages de programmation et la conception même du logiciel
par des méthodes mathématiques et non par des méthodes
empiriques basées sur le savoir-faire accumulé et l’expérience
(ce que l’on appelle en général l’ingénierie
du logiciel) dans une perspective d’amélioration de
qualité, de fiabilité et de sécurité.
Cet axe de recherche a démarré en 2006 avec la mise
en place de 3 projets :
Projet calculs sécurisés distribués et preuves
formelles
Chercheurs principaux :
• Cédric Fournet (Microsoft)
• James Leifer (INRIA)
Ces dix dernières années, les attentes en matière
de sécurité ayant évolué, la demande d’écriture
de code sécurisé s’est accrue et complexifiée.
Une bonne partie de la programmation a maintenant des conséquences
sur la sécurité des systèmes informatiques, que
les programmeurs s’efforcent de garantir et d’analyser.
Dans ce projet il est prévu de concevoir des outils formels
pour programmer simplement des calculs distribués, intégrant
des garanties de sécurité. L’objectif est de permettre
au programmeur d’exprimer et de prouver les propriétés
de correction, moyennant un effort raisonnable, qu’il soit automatique
ou parfois en partie manuel, dans le cadre du processus de développement
des programmes.
Projet composants mathématiques
Chercheurs principaux :
• Georges
Gonthier (Microsoft)
• Benjamin
Werner (INRIA)
L’objet du projet est d’établir que les théories
mathématiques formalisées peuvent, à l’image
de logiciels modernes, être construites à partir de composants.
Le terme « composant » est entendu comme un module
décrivant à la fois les aspects statiques (objets et
propositions) et dynamiques (preuves et méthodes de calcul)
d’une théorie. La proposition est ici de développer
une plate-forme générale pour les composants mathématiques,
construite sur l’extension de Coq utilisée pour la démonstration
du théorème des quatre couleurs. La validation de cette
plate-forme est envisagée à travers deux développements
significatifs: une théorie efficace de l’arithmétique
et la preuve du théorème de Feit-Thompson. Le premier
de ces travaux pourrait lui-même être utilisé dans
la résolution de différents défis remarquables
de formalisation mathématique, parmi lesquels la démonstration
en Coq de la preuve de Hales pour la conjecture de Kepler. Le second
serait une étape décisive pour pouvoir lancer un effort
collaboratif à grande échelle vers un nouveau défi
de preuve formelle: la classification des groupes simples finis.
Projet Outils et Méthodologies pour la spécification formelle et les preuves
Chercheurs principaux :
• Damien
Doligez (INRIA)
• Stephan Merz (INRIA)
• Leslie Lamport (Microsoft)
Le but de ce projet est de construire un système pour vérifier
mécaniquement les preuves de systèmes spécifiés
en TLA+. TLA+ est un langage formel de très haut niveau pour
les spécifications d'algorithmes et de systèmes. Ce langage
utilise les bases usuelles des mathématiques, comme la théorie
des ensembles enseignées à l'école secondaire
et en premier cycle, ou aussi utilisées par Bourbaki. TLA+ possède
un vérificateur de modèles (model checker) qui
permet de mettre au point les spécifications TLA+. Cependant,
de nombreuses spécifications sont trop complexes pour être
vérifiées sur des modèles suffisamment grands
pour détecter les erreurs les plus subtiles, et dans la plupart
des cas la vérification de modèles ne fournit pas le
niveau de confiance requis pour les applications critiques. Une preuve
mathématique vérifiée par la machine résout
ces problèmes en garantissant que la spécification vérifie
les propriétés énoncées dans tous les
modèles, quelle que soit leur taille, et même s'ils sont
infinis.
Défi scientifique : À travers cet axe de recherche
il est question d’améliorer considérablement la
qualité réelle
et perçue du logiciel et également de montrer que l’informatique
peut également permettre de démontrer des théorèmes
mathématiques qui sont en attente de l’être parfois
depuis des centaines d’années (on appelle cela une conjecture).
En 2005, Georges Gonthier a de cette manière démontré le « théorème
des 4 couleurs » - en attente de démonstration irréfutable
depuis 150 ans, il compte s’attaquer maintenant de cette manière à la
conjecture de Kepler : la « conjecture de
Kepler » concerne l'empilement des sphères (ou des
boulets de canons) dans un volume minimal. Celle-ci n'a été démontrée
par Hales qu'en 2003 et encore pas tout-à-fait suivant les critères
des mathématiciens. Elle énonce que l'empilement des
sphères dans l'espace le plus dense est celui du marchand des
quatre saisons à savoir le cubique face centrée (voir système
cristallin). Cette conjecture était en attente de démonstration
depuis plus de 350 ans !
Le second axe de recherche concerne les outils informatiques pour
les Sciences.
Au sein de cet axe de recherche plusieurs projets seront progressivement
démarrés en 2007, parmi ceux-ci le projet « Re-Activity » qui
sera présenté lors de l’inauguration et qui est
la concrétisation d’une collaboration entre
Wendy
MacKay et Mary Cswersinsky, chercheur senior à Microsoft
Research à Redmond, USA.
