Study of the Formal Verification of Compilers

This page describes an exercise on compiler verification based on the lecture given by Xavier Leroy at the DeepSpec Summer School in 2017. The goal is to get the students familiar with the basics concepts in compiler verification by doing the Coq project coming along with the lecture.

Course Materials

• Course website: https://xavierleroy.org/courses/DSSS-2017/
• Course slides: https://xavierleroy.org/courses/DSSS-2017/slides.pdf
• Course videos:
  • Lecture 1
  • Lecture 2
  • Lecture 3
  • Lecture 4
• Course exercises: https://github.com/DeepSpec/dsss17. Note that the Coq code is under the directory "compiler" which depends on the code in "lf".

Contents

The exercises is divided into the following parts:

• First, we study the basics of compiler verification, including
  • the syntax of the languages and the compilation of Imp to virtual machine code;
  • the big-step and small-step operational semantics;
  • verifying the compilation of terminating and non-terminating programs using simulations.
  For this, we are going to watch the videos of the first two lectures, and complete the exercises in Semantics.v, Sequences.v and Compiler.v.
• Second, we are going to study the verification of compiler optimizations, including
  • the liveness analysis and the verification of dead code optimization;
  • the verification of register allocation.
  For this, we are going to watch the videos of the third lecture, and complete the exercises in Fixpoint.v, Deadcode.v and Regalloc.v.
• Finally, we are going to watch the video of the last lecture to get a basic understanding of CompCert.

Schedule

• First meeting: 9:30--12:00 and 1:30--4:00, Oct 18th, 2020. Tencent Meeting Room: 365 2422 4847
• Second meeting: 9:30--12:00 and 1:30--4:00, Oct 25th, 2020. Tencent Meeting Room: 365 2422 4847