My project will involve adding additional functionality to the Bedrock 2 project. The goal of the Bedrock 2 project is to have a formally verified compiler for a low-level, C-like language. This allows for reasoning about compiler behavior and, therefore, trust surrounding compiled programs. Part of my work will be to develop proofs about the worst-case execution of compiled programs. This will allow for software to be compiled in a manner such that it is both provably correct and has provable performance characteristics.

Through this SuperUROP project, I am hoping to use my prior experience in compiler development applied in a much more focused area of research. I am really excited to learn more about the area of verification and be able to use it for practical applications within the compiler.