The course schedule is shown below. Slides will be posted after each lecture. If multiple papers are listed for a lecture, you are only expected to read the first one.
| Date | Topic | Slides | Reading | Assigned | Due |
|---|---|---|---|---|---|
| Jan 04 | Introduction & SAT Solving | L01 | [1] | ||
| Jan 06 | A Modern SAT Solver | L02 | [2][3] | ||
| Jan 11 | Applications of SAT | L03 | [4] | HW1 | |
| Jan 13 | SAT Modulo Theories | L04 | [5] | ||
| Jan 18 | A Survey of Theory Solvers | L05 | [6] | ||
| Jan 20 | Combining Theories | L06 | [7] | ||
| Jan 25 | The DPLL(T) Framework | L07 | [8] | ||
| Jan 27 | Finite Model Finding | L08 | [9] | HW2 | HW1 |
| Feb 01 | Reasoning about Programs I | L09 | [10] | ||
| Feb 03 | Reasoning about Programs II | L10, vcg.rkt | [11] | Proposal | |
| Feb 08 | No class, hack day! | ||||
| Feb 10 | Verification | L11, RingBuffer, Lemma, ED5C, VRhw | [12] | ||
| Feb 15 | Bounded Verification | L12 | [13][14][15] | HW3 | HW2 |
| Feb 17 | Symbolic Execution | L13 | [16] | ||
| Feb 22 | Angelic Execution | L14 | [17][18][19] | ||
| Feb 24 | No class, hack day! | ||||
| Mar 01 | Program Synthesis | L15 | [20] | HW3 | |
| Mar 03 | Solver-Aided Languages | L16 | [21] | ||
| Mar 08 | Metasketches | L17 | [22] | ||
| Mar 10 | Project Demos | Demo, Report, Prototype |