Le compilateur CompCert a été récompensé par la prestigieuse Association for computing machinery (ACM), pour la seconde fois
CompCert est le premier compilateur optimisant plusieurs architectures et utilisé dans l'industrie, qui soit doté d’une preuve mathématique de correction vérifiée par ordinateur.
Développé par plusieurs chercheurs* dont Sandrine Blazy, Professeure à l’Université de Rennes, directrice adjointe de l’IRISA et membre de l’équipe de recherche Epicure, ce compilateur a été récompensé avec l’obtention de ACM Software System Award (juin 2022) et dernièrement avec l’obtention de l’ACM SIGPLAN Programming Languages Software Award (janvier 2023).
Pour en savoir plus ... A lire sur le site du CNRS
CompCert récompensé par l’ACM pour ses garanties d’absence de bugs
Les compilateurs sont des programmes chargés de traduire le code des développeurs en des instructions directement compréhensibles par les machines. Premier compilateur offrant une garantie mathématique de son exactitude, CompCert a été récompensé, à deux reprises, par la prestigieuse Association for computing machinery (ACM). Il a été développé par plusieurs chercheurs issus du CNRS, d’Inria et des universités françaises... A lire sur le site du CNRS
Sandrine Blazy, Professeure à l’Université de Rennes et directrice adjointe de l’IRISA et ses collègues collègues Xavier Leroy, Collège de France; Zaynah Dargaye, Nomadic Labs; Jacques-Henri Jourdan, CNRS, Laboratoire Méthodes Formelles; Michael Schmidt, AbsInt Angewandte Informatik; Bernhard Schommer, Saarland University, and AbsInt Angewandte Informatik GmbH; and Jean-Baptiste Tristan, Boston College