Certifying Compiler for a C-like Programming Language

Compiler is complex software. Some compiler bugs are tricky to be found out by testing. How can one trust the compiler? One method is by providing a certified compiler. Formal proofs are given that semantic of source programs is preserved during compilation. It is nearly impossible to prove the full correctness of a practical compiler since compilation phases (including optimizations) are too complex and the algorithms are hard to be certified.
As another method, a certifying compiler needs to be implemented which can generate proofs when producing assembly codes. The generated proof is a formal proof that the produced codes confirm to their specifications. The code consumer needs not to trust the compiler nor the code producer. It only needs to run a proof checker before executing the codes.
However, the design of a certifying compiler is full of challenges and choices. Usually, certifying compiler cooperates with an automated theorem prover.
CComp is an on-going project. CComp is a certifying compiler for a C-like programming language Clike. The target language is x86 assembly language. We have designed a program logic ( an extension to Hoare logic ) for Clike using a fragment of separation logic and constrained first-order logic. There are several intermediate languages which are carefully chosen.
The main research aspects are:
● Trade off between expressivity and automation. Finding such a trade-off is non-trivial. Automation of the proof is vital, but the language and logic should be used to develop system software.
● Proof translation, that is, how to reuse the proof at source-level and build the lower level proof.
The goal of this research is to provide a practical tool for building large-scale proof-carrying system software.
websvn :

ccomp.zip7.21 MB
simplex.tar_.gz21.31 KB