Doctoral Speaking Skills Talk - Cayden Codel

— 4:00pm

Location:
In Person - Newell-Simon 3305

Speaker:
CAYDEN CODEL, Ph.D. Student, Computer Science Department, Carnegie Mellon University
http://crcodel.com/

Verified Substitution Redundancy Checking for SAT Solving

One reason for the widespread adoption of SAT solvers is that they are trustworthy: their answers can be checked with verified software. In particular, many SAT solvers can emit proof certificates of unsatisfiability that are efficient to check. However, the standard proof systems in use today struggle to succinctly express proofs for problem instances with a high degree of symmetry. 

In this talk, we discuss our recent work on proof checking tools for the substitution redundancy (SR) proof system. We discuss a few problems that admit short SR proofs, as well as how we can express and check those proofs. Our verified proof checker was developed in the Lean theorem prover. 

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement

Event Website:
https://csd.cmu.edu/calendar/doctoral-speaking-skills-talk-cayden-codel