| Date | Lesson # | Topics | Reference | HW |
|---|---|---|---|---|
| 31.12.23 | 1 |
Software Verification with SAT
Propositional Logic CNF DIMCAS |
Chapters 1,2 of Decision Procedures
Chapter 1 of Calculus of Computation verification2.cnf |
|
| 7.1.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 21.1.23 |
| 14.1.24 |
3 |
Horn Formulas DPLL |
Linear-time algorithms for testing the satisfiability of ... by Dowling and Gallier Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
|
| 21.1.24 | 4 | DPLL |
Chapter 2 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
HW 2 Due 11.2.24 |
| 28.1.24 | -- | MILUIM week | ||
| 4.2.24 |
5 |
Intro to First-order Logic Fucntional Signatures Semantics of Functional Signatures Congruence Closure: Calculus |
Chapters 2, 9.1, 9.2 of Calculus of Computation Chapter 4 of Decision Procedures uf.smt2 cvc5 |
|
| 11.2.24 | 6 | Congruence Closure: Correctness |
Chapter 4 of Decision Procedures Chapters 9.1, 9.2 of Calculus of Computation |
HW 3 Due 25.2.24 |
| 18.2.24 | 7 | DPLL(UF) |
Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al.
CAV Award Example of industrial smt2 file |
|
| 25.2.24 |
8 |
DPLL(UF) General Signatures |
Chapter 3 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. CAV Award Example of industrial smt2 file |
|
| 3.3.24 | 9 |
General Signatures Arithmetic Many-sorted Signatures |
Chapters 2 -- 3 of Calculus of Computation Chapters 3--5 of Decision Procedures |
|
| 10.3.24 | 10 |
Arrays Quantifiers |
Chapter 7 of Decision Procedures Chapters 2, 3.6 and 9.5 of Calculus of Computation arrays_uf.smt2 arrays.smt2 |