The compiler is a tool that is central to the development of software. Its role is to translate the human-readable code written by a programmer into machine code that a computer can understand. Because the compiler creates the actual machine code that runs on the computer, a faulty compiler can lead to catastrophic failures, including errors in medical devices, in fly-by-wire aviation software, and in automotive systems. This research will lead to more reliable compilers, which in the end will increase our confidence in the software that has now become ubiquitous and safety-critical in our daily lives.
This project will develop new techniques for building compilers to ensure the utmost level of rigor and reliability, so that we can know with certainty that the machine code running on the computer does exactly what the programmer intended it to do. To achieve this goal, the principal investigator will investigate ways of using proof assistants to implement formally verified compilers. More specifically, the research will explore techniques for making formally verified compilers like Compcert generate better code, so that they can be more competitive with mainstream compilers like GCC and LLVM. Furthermore, the research will also investigate ways of decreasing the proof burden, so that verified compilers like Compcert can be developed and updated more easily. In the end, this research will enable formally verified compilers to become more mainstream, so that they can used more broadly by programmers.
