Xavier Leroy of the Paris-Rocquencourt research center of INRIA, France, is the recipient of the 2012 Microsoft Research Verified Software Milestone Award. The award is given in recognition of Xavier's role as architect of the CompCert C Verified Compiler as well as his leadership of the development team.
The formal presentation of the Award will be made to Xavier at POPL 2013, which will take place in Rome, January 23-25, 2013.
The full award citation can be accessed here. Its executive summary reads:
"Microsoft Research is delighted to celebrate the advances made by Dr Leroy in the vital field of software verification. Compilers are the basis for all the software we generate, and by ruling out compiler-introduced bugs, the CompCert project has taken a huge leap in producing strengthening guarantees for reliable critical embedded software across platforms. We congratulate Dr Leroy on his significant achievement in winning this Award."
Congratulations to Xavier for this important recognition of his long-term work on CompCert.
No comments:
Post a Comment