Thomas Raymond Carotti

Thomas Raymond Carotti

Scholar Title

Undergraduate Research and Innovation Scholar

Research Title

Implementing Additional Functionality for a Verified Compiler




Electrical Engineering and Computer Science

Research Areas
  • Software Design and Programming Languages

Adam Chlipala


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.”

Back to Scholars