Research Project Title:
Implementing Additional Functionality for a Verified Compiler
abstract: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."