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.

Comments are closed