I’m a third-year PhD student in the Computer Science Department at Carnegie Mellon University. I’m co-advised by Prof. Marijn J. H. Heule and Prof. Jeremy Avigad.
My work focuses on the intersection of theorem proving and SAT solving. In particular, I use the Lean interactive theorem prover to make SAT solving tools more trustworthy. I’m currently working on the Trestle and Verus projects.
I have yet to leave CMU: I graduated from CMU with my master’s in computer science in 2022, and I graduated from CMU with my BS with honors in computer science in 2021.
Coordinates
My email is: ccodel [at] andrew [dot] cmu [dot] edu.
I work in office GHC 9005, on the ninth floor of the Gates-Hillman Center on CMU’s Pittsburgh campus.
News
- My advisor’s result on the Empty Hexagon Problem was recently featured by Purple Mind in a video on YouTube. Our lab’s verification of the result appears in the video as well. Give it a watch!
- In October 2024, I gave a talk at FMCAD on my verified SR checking work. You can watch a version of the talk on YouTube.
Employment
- Summer 2024: Applied Scientist Intern for the Automated Reasoning Group at AWS in Seattle. My manager was Leonardo de Moura, and I worked closely with Emina Torlak and Arash Maymandi. I used Lean to formalize parts of the PartiQL database query language.
- Summer 2023: Research consultant for Starkware Industries, a smart contracts company based in Israel. I worked with Yoav Seginer and my advisor Jeremy Avigad. I used Lean to formally verify standard library functions for Starkware’s smart contracts language Cairo.
- Summer 2022: Applied Scientist Intern for the Automated Reasoning Group at AWS in NYC. My manager was Robert Jones, and I worked closely with fellow PhD student Hanna Lachnitt, AWS scientist Bruno Dutertre, and my advisor Marijn Heule. Our work was eventually published at FMCAD 2024.
- Also summer 2023, 2024: Volunteer research mentor for Lumiere Education. I guided high school students’ computer science research projects.
Teaching
I have had the pleasure of being a teaching assistant for several courses at Carnegie Mellon University. Undergraduate students at CMU are encouraged to TA for introductory-level CS classes, while PhD students are required to TA at least twice during their studies. Below is a listing of the courses and semesters I was a TA:
- 15-410: Operating System Design and Implementation (F24, S21, F20, S20)
- 15-414: Bug Catching: Automated Program Verification (S24)
- 15-210: Parallel and Sequential Data Structures and Algorithms (F21, F19, S19)
- 15-213: Introduction to Computer Systems (Summer 20)
Service
- Tea brewer extraordinaire, CMU Computer Science Department weekly tea, F23 - S25
- Artifact evaluation committee, CAV 2025
- Organizer, CMU Computer Science Department Programming Languages lunch (“PLunch”), F23 - S24
- Artifact evaluation committee, CAV 2023