The FME Lucas Award goes to Sandrine Blazy, Zaynah Dargaye and Xavier Leroy for their paper
published at the 14th International Symposium on Formal Methods (FM 2006).
Sandrine Blazy receives the Lucas Award
The FME Awards Committee motivated its decision as follows:
CompCert is a landmark in program verification and formal methods in general, with real-world applications still very active today. (A new version was released just a couple of months ago.) The CompCert team, including the authors of this paper, received, in 2021, the ACM Software System Award. It recognizes “a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both” and is considered the highest award for software originating from computer science research.This is the paper that pushed the CompCert verified compiler idea into real use by supporting the widely used C language front-end in a provable way. This is, therefore, a highly influential piece in the series of works that led to the first verified compiler. This has not only had a major impact in the theory of verification, but also made the case for applying formal methods in mission-critical cases, where the entire tool chain has to be certified.
The paper is available here.