The Microsoft Research Verified Software Milestone Award is made to Xavier Leroy for the CompCert Project. The award is given in recognition for Xavier's role as architect of the CompCert C Verified Compiler as well as his leadership of the development team.
The CompCert Project formally verified an industrial strength C compiler, which is compliant with the ISO-C-90 and ANSI-C standards with only a few principled exceptions and extensions. The compiler generates efficient code for PowerPC, ARM and x86 processors. The verification effort focused on the
core aspects of the compilation process - some 14 passes and 11 intermediate languages.
The scale of the CompCert C Compiler is unprecedented within the formal verification community. The CompCert Project reflects the essence of the Verified Software Initiative - it has addressed the challenges of large-scale software verification, bringing together theories, tools and experiments. Traditional software verification technologies focus on the correctness of source code. CompCert complements these technologies by providing formal guarantees that the verified source code is correctly translated into executable code.
The CompCert Project was started in 2005, and the development of the compiler continues apace. For instance in the summer of 2012 floating-point arithmetic was fully formalised and verified. With complete sources publicly available, the impact of the CompCert Project will only continue to grow.
MRS Award >