I’m a fourth-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.
CMU continues to be my academic home: 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
- We received the best paper award at SAT 2026 for our work on symmetry breaking for SAT, “Simplify, Order, Break, Repeat”, and our SAT solver won the SAT Competition 2026.
- We received a distinguished paper award at TACAS 2026 for our work on “Orbitopal Fixing in SAT”.
- 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!
Employment
- Summers 2022, 2024, 2025, 2026: Applied Scientist Intern for the Automated Reasoning Group at AWS. My manager was Robert Jones every summer except for 2024, when it was Leonardo de Moura. In 2022 and 2026, I worked on the eDRAT proof format for SMT solving, which was ultimately published at FMCAD 2024. In 2024, I worked with Emina Torlak and Arash Maymandi to formalize parts of the PartiQL database query language. In 2025, I updated the scripts used to run the parallel and distributed SAT/SMT competitions on AWS, and as a byproduct of my work, I ran the 2025 parallel SAT competition. The scripts can be found on GitHub here.
- 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.
- Also summer 2023, 2024: Volunteer research mentor for Lumiere Education. I gave feedback on 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 social, F23 - S26.
- Organizer, 2025 parallel SAT competition. (Main page here, organizer page here.)
- Artifact evaluation committee, CAV 2025 and CAV 2023.
- Organizer, CMU Computer Science Department Programming Languages lunch (“PLunch”), F23 - S24.