The course schedule is shown below. Slides will be posted after each lecture. Additional readings will be posted as well. If multiple references are listed for a lecture, you are only expected to read the first one. The rest are optional.
| Date | Topic | Slides | Reading | Assigned | Due |
|---|---|---|---|---|---|
| 03/30 | Introduction & SAT Solving | L1 | [1] | ||
| 04/01 | A Modern SAT Solver | L2 | [2] [3] | ||
| 04/06 | No class, plan your project! | HW1 | Project Team | ||
| 04/08 | Applications of SAT | L3 | [4] | Project Topic | |
| 04/13 | SAT Modulo Theories | L4 | [5] | ||
| 04/15 | A Survey of Theory Solvers | L5 | [6] | Project Proposal | |
| 04/20 | Combining Theories | L6 | [7] | HW2 | HW1 |
| 04/22 | The DPLL(T) Framework | L7 | [8] | ||
| 04/27 | Finite Model Finding | L8 | [9] | ||
| 04/29 | Reasoning about Programs | L9 | [10] | ||
| 05/04 | Verification | L10, rb1.dfy, rb2.dfy | [11] | HW3 | HW2 |
| 05/06 | Bounded Verification | L11 | [12] [13] [14] | ||
| 05/11 | Symbolic Execution | L12 | [15] | Project Progress | |
| 05/13 | Model Checking I | L13 | [16] [17] | ||
| 05/18 | Model Checking II | L14 | [18] | HW4 | HW3 |
| 05/20 | Program Synthesis | L15 | [19] | ||
| 05/25 | Angelic Execution | L16 | [20] [21] [22] | ||
| 05/27 | Solver-Aided Languages | L17 | |||
| 06/01 | No class, hack day! | HW4 | |||
| 06/03 | Project Demo | Project Report & Code |