Doctoral Speaking Skills Talk - Cayden Codel November 14, 2024 3:00pm — 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 Add event to Google Add event to iCal
