| Date | Lesson # | Topics | Reference | HW |
|---|---|---|---|---|
| 06.03.22 | 1 |
Software Verification with SAT Propositional Logic CNFization |
Chapters 1+2 of Decision Procedures
Chapter 1 of Calculus of Computation |
|
| 13.03.22 | 2 |
CNFization DIMACS Polynomial cases of SAT |
Chapter 2 of Decision Procedures
Chapter 1 of Calculus of Computation Linear-time algorithms for testing the satisfiability of ... by Dowling and Gallier The Complexity of Satisfiability Problems by Schaefer |
|
| 20.03.22 | 3 | DPLL: Calculus DPLL: Implementation |
Chapter 2 of Decision Procedures
Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
HW 1 |
| 27.03.22 | 4 | DPLL: Correctness Software Verification with FOL |
Chapters 2 and 4 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. A termination proof of DPLL |
|
| 03.04.22 | 5 | Functional Signatures Semantics Flat Cubes |
Chapter 2 of Calculus of Computation Chapter 4 of Decision Procedures |
|
| 10.04.22 | 6 | Congruence Closure: Calculus Congruence Closure: Implementation |
Chapter 4 of Decision Procedures Chapters 9.1, 9.2 of Calculus of Computation An example of an smt2 file An example of a python file that uses pysmt The SMT-LIB Standard |
HW 2 |
| 17.04.22 | -- | No Class | ||
| 24.04.22 | 7 | Congruence Closure: Correctness Intro to DPLL(UF) |
Chapters 3-4 of Decision Procedures Chapter 9.2 of Calculus of Computation Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
|
| 01.05.22 | 8 | DPLL(UF): Calculus DPLL(UF): Correctness |
Chapter 3 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
|
| 08.05.22 | 9 | DPLL(UF): Correctness General Signatures |
Chapter 2 of Calculus of Computation Chapters 3--4 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
|
| 15.05.22 | 10 |
General Signatures Arithmetic The Install Problem |
Chapters 2--3 of Calculus of Computation Chapter 5 of Decision Procedures Opium: Optimal package install/uninstall manager by Tucker et al. |
|
| 22.05.22 | 11 | Many-sorted Signatures Bit-vectors |
Chapter 6 of Decision Procedures | HW 3 |
| 29.05.22 | -- | No Class | ||
| 05.06.22 | -- | No Class | ||
| 12.06.22 | 12 | Quantifiers Arrays |
Chapter 7 of Decision Procedures Chapters 3.6 and 9.5 of Calculus of Computation |
|
| 19.06.22 | 13 | Arrays Summary |
Chapter 7 of Decision Procedures Chapters 3.6 and 9.5 of Calculus of Computation |