CompCert et compilateurs certifiés

Xavier Leroy

Collège de France

Science du logiciel

Année 2018-2019

Leçon inaugurale : Le logiciel, entre l'esprit et la matière.

Les travaux de recherche de Xavier LEROY portent d'une part sur les nouveaux langages et outils de programmation, et d'autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l'un des principaux développeurs du langage de programmation fonctionnelle OCaml ainsi que du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.

Langages fonctionnels, systèmes de types et mise en pratique : les langages Caml Light et OCaml

Xavier LEROY a été formé aux mathématiques et à l'informatique à l'École normale supérieure, puis à l'INRIA où il a effectué sa thèse. Programmeur prodige, il s'est illustré par une série de travaux de premier plan sur les systèmes de types et les systèmes de modules pour les langages fonctionnels, qui ont abouti au développement de Caml Light, devenu aujourd'hui OCaml, l'un des deux langages fonctionnels typés les plus utilisés au monde, dans des domaines aussi divers que l'aéronautique, la finance ou encore le Web. Ce langage est le support de développement d'outils logiciels très variés comme l'assistant de preuve Coq, les analyseurs statiques Astrée et Frama-C, le compilateur SCADE 6 d'Estérel Technologies et la blockchain Tezos. OCaml a été utilisé dans de nombreux projets emblématiques comme la version web de Facebook Messenger, le logiciel MediaWiki ou encore l'infrastructure de virtualisation Docker.

Preuve de programme, preuve de compilateurs et mise en pratique : le compilateur CompCert

Xavier LEROY est également à l'origine de CompCert, qui est un compilateur C certifié, écrit et vérifié grâce à l'assistant de preuve Coq. Il s'agit d'une première mondiale à plusieurs titres : il autorise une vérification formelle d'une taille et d'une complexité sans précédent, et surtout, il offre la possibilité de disposer d'un compilateur certifié, étape clé dans la certification et la vérification automatique des chaînes logicielles, et donc vers la programmation « zéro défaut ». Ce fait d'arme a eu un impact considérable sur la nature même des grands programmes de recherche sur les logiciels.

Nommé professeur au Collège de France, Xavier LEROY occupera la chaire Sciences du logiciel où il dispensera dès l'année académique 2018-2019 une série de cours intitulée Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui.

Leçon inaugurale jeudi 15 novembre 2018 à 18h00