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 Lineartime 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 SMTLIB Standard 
HW 2 
17.04.22    No Class  
24.04.22  7  Congruence Closure: Correctness Intro to DPLL(UF) 
Chapters 34 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 34 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. 

15.05.22  10 
General Signatures Arithmetic The Install Problem 
Chapters 23 of Calculus of Computation Chapter 5 of Decision Procedures Opium: Optimal package install/uninstall manager by Tucker et al. 

22.05.22  11  Manysorted Signatures Bitvectors 
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 