PhD Defense of Pierre Wilke
Pierre Wilke has successfully defended his PhD on “Formally verified compilation of low-level C code”, covering his work on building a formally verified compiler providing the same level of guarantee as CompCert, but for C programs that perform low-level operations, in particular on the binary representation of pointers.
