| Date | Lesson # | Topics | Reference | HW |
|---|---|---|---|---|
| 3.11.24 | 1 |
Software Verification with SAT
Propositional Logic CNF |
Chapters 1,2 of Decision Procedures
Chapter 1 of Calculus of Computation verification2.cnf |
|
| 10.11.24 | 2 |
CNF Horn Formulas |
Chapter 1 of Calculus of Computation Linear-time algorithms for testing the satisfiability of ... by Dowling and Gallier |
HW 1 Due 4.12.24 |
| 17.11.24 | 3 | DPLL | Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. | |
| 24.11.24 | 4 |
DPLL correctness CDCL |
Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. Slides about DPLL and CDCL by Cesare Tinelli. |
|
| 1.12.24 | 5 |
Fucntional Signatures Congruence Closure: Calculus |
Chapters 2, 9.1, 9.2 of Calculus of Computation Chapter 4 of Decision Procedures uf.smt2 cvc5 |
HW 2
Due 25.12.24 |
| 8.12.24 | 6 |
Congruence Closure: Correctness |
Chapter 4 of Decision Procedures Chapter 9.2 of Calculus of Computation |
|
| 15.12.24 | 7 | DPLL(UF) |
Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al.
CAV Award |
|
| 22.12.24 | 8 |
|
||
| 29.12.24 |
-- | Hanukkah | ||
| 5.1.25 | 9 |
HW 3 Due 5.2.25 |
||
| 12.1.25 | 10 | |||
| 19.1.25 | 11 |
HW 4 (RESHUT)
Due 5.2.25 |
||
| 26.1.25 | 12 | |||
| 2.2.25 | 13 |