Eric Mullen, General Examination

Title: Pushing the Limits of Compiler Verification

Advisors: Dan Grossman and Zach Tatlock

Supervisory Committee: Dan Grossman (co-Chair), Zach Tatlock (co-Chair). Geoffrey Paul Boers (GSR, Music), Xi Wang, and Paul Beame

Abstract: The CompCert formally verified compiler has been repeatedly shown to have a strong formal guarantee. However, there are still limits to compiler verification: both a semantic gap between the lowest level of the compiler and the hardware, and unverified extraction being trusted near the top. Here I describe how I am pushing the limits of compiler verification, by working to both close the low level semantic gap and remove our reliance on unverified extraction.