Sandrine BlazySciences du logiciel

Professeure à l’université de Rennes, membre de l’Institut de recherche en informatique et systèmes aléatoires1 , spécialiste de sciences du logiciel.

Les recherches de Sandrine Blazy visent au développement de logiciels sûrs. Sa contribution se concentre sur les outils informatiques qui permettent à un programme écrit de devenir exécutable : les compilateurs. Traditionnellement, ces outils indispensables 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 : c’est un apport majeur pour les sciences du logiciel. Depuis 2003, elle développe, avec Xavier Leroy, CompCert, le premier compilateur pour le langage C vérifié à l’aide de Coq. Il est commercialisé par la société AbsInt, a été utilisé dans l’industrie avionique et le nucléaire, domaines où la fiabilité logicielle est primordiale, et est disponible pour la recherche. Elle poursuit ses travaux pour doter CompCert de davantage de possibilités de compilation, et offrir des garanties supplémentaires en termes de sécurité logicielle.
 

• Institut de recherche en informatique et systèmes aléatoires
• Délégation Bretagne et Pays de la Loire
• Institut des sciences de l'information et de leurs interactions

• 1CNRS/Université de Rennes