| Date | Topic | Slides | Deadlines |
|---|---|---|---|
| 1/14 | Course Overview, Floyd-Hoare Logic | Intro; Verification Pre-History | -- |
| 1/21 | Review of Floyd-Hoare Logic, Dijkstra's WP calculus, Intro to LTS | Labeled Transition Systems | -- |
| 1/28 | Program Graphs to LTS, Concurrent Systems | " | -- |
| 2/4 | LTS: equivalences, bisimulations | " | -- |
| 2/11 | LTS: Simulation Relations, Safety Properties | Safety, Liveness, Fairness | -- |
| 2/18 | Liveness, Fairness, Intro to Büchi automata | Omega-automata | HW1 assigned |
| 2/25 | ω-automata, intro to LTL | " | -- |
| 3/4 | Timed Automata and Verification | Slides | HW2 due |
| 3/11 | Metric and Signal Temporal Logic | Slides | HW3 assigned |
| 3/18 | No class, Spring Break | -- | -- |
| 3/25 | Probablistic Verification: I | Slides | HW3 due |
| 4/1 | Probabilistic Verification: II | Slides | HW4 assigned |
| 4/8 | Hybrid and Nonlinear Systems Verification : I | Slides | -- |
| 4/15 | Hybrid and Nonlinear Systems Verification : II | Slides | HW4 due |
| 4/22 | Neural Network Verification | Slides | -- |
| 4/29 | Schedule overflow | -- |