Intervention de Michel Cosnard

a déclaré bien connaître le projet Grid'5000, puisqu'il en est l'initiateur. C'est une plate forme de recherche visant à créer une puissance de calcul grâce à une « grille » expérimentale de 5000 processeurs interconnectés à travers la France, via le réseau RENATER. A ce stade, l'interconnexion ne rassemble encore que 4000 processeurs environ. Dans la mesure où ce dispositif est tourné vers la recherche, il n'est mis à disposition de la communauté scientifique que pour des calculs non critiques. Un exemple d'utilisation concerne justement les calculs de simulation dans le cadre des recherches sur le stockage de longue durée des déchets radioactifs, domaine dans lequel l'ANDRA travaille en partenariat avec l'INRIA.

Pour bien faire comprendre l'intérêt des recherches communes sur la qualité des logiciels conduites depuis janvier 2007 avec Microsoft Research, M. Michel Cosnard a rappelé que le théorème d'incomplétude de Gödel, sur l'existence d'énoncés mathématiques indémontrables, avait pour conséquence qu'il était théoriquement impossible de concevoir une « boîte noire » qui permettrait de vérifier la parfaite adéquation d'un logiciel à un panel de spécifications. Mais cela n'empêche pas de pouvoir faire des vérifications complètes dans certains cas particuliers, notamment celui des petits programmes. Et des efforts très importants de vérification ont été effectués par les banques pour assurer la fiabilité de la carte à puce, ou par l'industrie aéronautique pour ses systèmes. En revanche, la culture de la fiabilité des logiciels est encore très peu répandue dans le milieu industriel en général.

Le laboratoire commun « INRIA - Microsoft Research » confie à une équipe organisée autour de Georges Gonthier et Benjamin Werner, les inventeurs d'une preuve formalisée du théorème des quatre couleurs, des recherches sur les méthodes de programmation permettant d'assurer leur qualité, leur fiabilité et leur sécurité. Le théorème des quatre couleurs prévoit qu'on peut décrire avec quatre couleurs une carte décomposée en zones contiguës ; ce résultat conjecturé en 1852 ne peut être démontré, compte tenu des milliers de cas possibles à traiter, sans un détour par un lourd calcul informatique, dont il faut justement certifier la fiabilité.

L'effort financier est supporté pour moitié par chaque partenaire. Pour Microsoft, il s'agit d'un investissement de long terme, qui va alimenter entre-temps un flux de conférences internes permettant aux salariés de rester attentifs aux progrès de la recherche fondamentale en informatique, avant peut-être d'aboutir à une percée technologique. Pour l'INRIA, c'est une manière de poursuivre ses objectifs stratégiques en partageant l'effort financier. Le choix des thèmes de recherche est soumis, comme pour les autres projets de l'INRIA, à un comité d'experts indépendants.