Vérification d'une preuve mathématique par ordinateur par Sandrine Blazy, médaille d'argent du CNRS 2023

Preuve mathématique vérifiée par ordinateur. La démonstration est menée au moyen de commandes écrites par l’utilisateur indiquant comment progresser, en interaction avec un assistant de preuve (à l'écran). Ce logiciel automatise une partie du raisonnement, s’assurant de la validité de la démonstration. Les recherches de Sandrine Blazy, lauréate de la médaille d'argent du CNRS 2023, visent au développement de logiciels sûrs et se concentrent sur les compilateurs, des outils informatiques qui permettent à un programme écrit de devenir exécutable. Traditionnellement, ils ne sont pas vérifiés avec des garanties mathématiques, et peuvent donc compiler un programme sûr en un programme exécutable contenant des bugs. Sandrine Blazy s’appuie sur la vérification déductive afin de garantir mathématiquement la correction de compilateurs. Avec Xavier Leroy, elle développe CompCert, le premier compilateur pour le langage C vérifié à l’aide de Coq. Commercialisé par la société AbsInt, il a été utilisé dans l’industrie avionique, le nucléaire et est disponible pour la recherche. Elle cherche à doter CompCert de davantage de possibilités de compilation, et offrir des garanties supplémentaires de sécurité logicielle.