Sandrine Blazy, Université de Rennes

Tuesday, November 26, 2024 18:00
Amphi 25, Sorbonne University - Faculté des Sciences

Compilation vérifiée : vers du logiciel zéro défaut

Sandrine Blazy est professeure à l'Université de Rennes et directrice adjointe de l'UMR IRISA. Sa thématique de recherche est la vérification formelle de logiciels afin de garantir leur sûreté et leur sécurité. Elle a reçu la médaille d’argent du CNRS en 2023. Avec six collègues, elle a reçu en juin 2022 le prix « ACM software system award » et en juin 2023 le prix « ACM SIGPLAN Programming Languages Software Award » pour le développement du compilateur vérifié CompCert.

La vérification déductive permet d’avoir des garanties très fortes sur l’absence de bug dans les logiciels; elle est utilisée pour développer des logiciels embarqués critiques, où toute erreur peut compromettre des vies humaines ou avoir d’autres conséquences catastrophiques. La vérification étant effectuée au niveau source, le compilateur, logiciel complexe et point de passage obligé pour obtenir un code écrit dans un langage compréhensible par la machine mais bien plus primitif, devient un maillon faible dans la chaîne de production du logiciel. Aussi, vérifier le compilateur lui-même permet de garantir qu’aucune erreur n’est introduite lors de la compilation. Plus généralement, cette approche ouvre la voie à la vérification des outils informatiques participant à la production et à la vérification du logiciel. Cet exposé présente les défis sémantiques qu’il a fallu résoudre pour développer CompCert, le premier compilateur optimisant ciblant plusieurs architectures et utilisé dans l'industrie, qui soit doté d’une preuve mathématique de correction vérifiée par ordinateur. Cette preuve se fonde sur un raisonnement sur la sémantique des programmes observés, c’est-à-dire une définition mathématique du comportement de ces derniers. Le code produit par CompCert est garanti se comporter comme prescrit par la sémantique du programme source C. Ce niveau de confiance dans la correction de la compilation permet à CompCert de répondre aux plus hauts niveaux de fiabilité logicielle.

One particularly popular moment associated to the colloquium is the “Master Class” where students have the opportunity to give a short (but well-prepared) presentation of his/her work. Each presentation (10 minutes) is followed by an open discussion with the guest speaker (15 minutes) who gives a detailed feedback. The complete program is provided here.

Electronic access

• Slides

• Offline video