Doctoral Thesis Proposal - Cayden Codel
— 10:30am
Location:
In Person and Virtual - ET
-
Gates Hillman 8102 and Zoom
Speaker:
CAYDEN CODEL
,
Ph.D. Student
Computer Science Department
Carnegie Mellon University
https://www.crcodel.com/
Automated reasoning (AR) tools are versatile and practically efficient pieces of software that can solve a wide variety of problems in industry and academia. One of their strengths is their ability to generate proofs checkable by verified software. Even if the AR tools themselves contain bugs (and they often do), we can still have a high degree of confidence in the correctness of their answers.
However, this verified toolchain can be extended further to include encodings. Usually, AR tools solve problems that have been encoded into a form that they can understand. This process of encoding can introduce bugs, meaning that the encoded form of the problem no longer accurately represents the original. Bugs are more likely to appear when the encoding is more complicated, such as when auxiliary logical objects are introduced in order to make the encoding smaller or easier for the AR tool to manipulate. Unfortunately, complicated encodings are becoming increasingly necessary in order to push the boundaries of what problems AR tools can solve. As a result, we argue that the standard AR toolchain should now include verified encodings by default.
In this thesis, we will develop an end-to-end verified toolchain for the boolean satisfiability problem (SAT) in the Trestle project. Trestle currently has a verified SAT proof checker and good support for writing verified encodings, but its encoding tools are complicated and hard to use, and only a handful of encodings have been verified so far. As a result, we plan to redesign how encodings are written in Trestle, and to verify new encodings. We also plan to add symmetry-breaking reasoning to Trestle and add features to enable end-to-end theorem proving with the use of SAT solvers.
Thesis Committee
Marijn Heule (Chair)
Jeremy Avigad
Bryan Parno
Benjamin Kiesl-Reiter (Amazon Web Services)
Additional Information
In Person and Zoom Participation. See announcement.
For More Information:
matthewstewart@cmu.edu