How to formally verify a compiler (frontend and/or backend)?

Question

For a project I am about to begin, I was exploring formal verification of a compiler. I came across the CompCert C Compiler which is an ACM awarded, formally verified C compiler.

When I read further, it mentioned that it has used Coq Proof Assistant to mechanise the automated verification.

The question is: How does one go about creating the proofs/theorems for instruction translation? What are the steps? Any guidance is welcome.

Answer 1

Xavier Leroy has given a class at Collège de France on the topic in 2019/2020¹. The lessons themselves are in French, but the excellent material is available in English here: https://github.com/xavierleroy/cdf-mech-sem . In particular, the files Imp.v and Compil.v will give you an excellent head start on the basics.

However jumping in the Coq code directly is likely to be tricky. Visiting first or in parallel Software Foundation as pointed out by kiner_shah is an excellent idea.

¹: https://www.college-de-france.fr/agenda/cours/semantiques-mecanisees-quand-la-machine-raisonne-sur-ses-langages

Answer 2

There is a much simpler compiler for pedagogical purposes in the coq-commmunity development named semantics

There is also a very elementary parser and more language related tools, like a tool to verify programs by weakest precondition, and an abstract interpreter (to prove that variables stay in some intervals).