| CS 745 Computer Aided Verification | Fall 2019 |
Below is the basic schedule of lectures along with associated readings from the text, I'll update this as we proceed.
| Date | Topic | Reading |
| Sep 5 | Course overview; Introduction | Handout |
| Sep 10 | Computation structures, temporal logic syntax | Chap. 1-4 |
| Sep 12 | Temporal logic semantics | Chap. 4 |
| Sep 17 | CTL Model Checking | Chap. 5 |
| Sep 19 | Fairness, Fair CTL model checking | Chap. 5 |
| Sep 24 | Automata on infinite strings | Chap 7 |
| Sep 26 | Composition of automata, language emptiness | Chap 7 |
| Oct 1 | LTL and CTL model checking | Chap 6 & 7 |
| Oct 3 | Compositional Reasoning | Chap 15 + `On the completeness of compositional reasoing', Namjoshi & Trefler, CAV 2000 |
| Oct 8 | Compostional Reasoning | |
| Oct 10 | Symmetry Reduction | Chap 17 |
| Oct 15 | reading week | |
| Oct 17 | reading week | |
| Oct 22 | Symmetry Reduction, Process Equivalence | `Symmetry and Model Checking,' Emerson and Sistla, CAV 1993, Chap 11 |
| Oct 24 | Analyzing Parametrized Systems | Chap 18 |
| Oct 29 | Propositional Mu-calculus | Chap 16 |
| Oct 31 | Mu-caluclus model checking | Chap 16 |
| Nov 5 | Compositional Local Reasoning | |
| Nov 7 | ||
| Nov 12 | ||
| Nov 14 | ||
| Nov 19 | ||
| Nov 21 | ||
| Nov 26 | ||
| Nov 28 | ||
| Dec | ||