Course Schedule
The schedule below is tentative and may change throughout the semester.
📹 Video recordings will be automatically added to Media Space immediately after class (registration is required to access these videos). I will not post every video link individually.
| Lecture | Date | Topic | Readings | Homework |
|---|---|---|---|---|
| L1 | 01/16 | Introduction (slides) | Ch1, Ch2 | |
| L2 | 01/18 | Modeling Computation, executions, invariance, reachability (slides) | Ch2 | |
| L3 | 01/23 | Proofs of inductive invariance properties, Satisfiability problem. (slides) | Ch 7.5 | HW1 out (due 02/11) |
| L4 | 01/25 | Solving SAT problem, DPLL algorithm (slides) | Ch 7.5 | |
| L5 | 01/30 | Satisfiability Modulo Theory (slides) | Ch 7 | |
| L6 | 02/01 | SMT, Linear Real Arithmetic and Simplex (slides) | Ch 7 | |
| L7 | 02/06 | Neural networks and machine learning systems; verification problem for ML-enabled systems (slides) | ||
| L8 | 02/08 | Verification as optimization problems; Integer programming and linear programming formulations for neural network verification (slides) | papers: MILP formulation, LP formulation | |
| L9 | 02/13 | Bound propagation algorithms for neural network verification (slides) | papers: CROWN Convex-relaxation-barrier | |
| L10 | 02/15 | Branch-and-bound for neural network verification (slides) | papers: beta-CROWN Branch-and-bound | |
| L11 | 02/20 | From algorithms to real-world NN verifiers; falsification, training of verifiable networks (slides) | papers: VNN-COMP PGD attack IBP training | HW2 out (due 03/10) |
| L12 | 02/22 | Modeling physics, dynamical systems (slides) | Ch 3 | |
| L13 | 02/27 | Dynamical systems (Part II); discuss some ideas on class projects (slides) | Ch 3 | |
| L14 | 02/29 | Stability analysis of dynamical systems (slides) | Ch 10.5 papers: Lyapunov-stable neural-network control | Project proposal due 3/3 |
| L15 | 03/05 | Modeling cyberphysical systems. Hybrid automata (slides) | Ch 4 | |
| L16 | 03/07 | CPS Invariants; intro to CTL (slides) | Ch 4, Ch 7 | |
| Spring break | 03/12 | No class | ||
| Spring break | 03/14 | No class | ||
| L19 | 03/19 | intro to CTL; CTL model checking (slides) | Ch 6 | |
| L20 | 03/21 | CTL model checking, intro to timed automaton (slides) | Ch 6, 9 | |
| L21 | 03/26 | Mid-semester project review | Midterm presentation slides due 3/25 | |
| L22 | 03/28 | Mid-semester project review | Presentation feedback due 3/29 | |
| L23 | 04/02 | Guest lecture (Prof. Richard Y. Zhang): Semidefinite-programming-based neural network verification | Paper: Low Rank SDP for NN verification | This guest lecture is in-person |
| L24 | 04/04 | Guest lecture (Prof. Saber Jafarpour): Mixed-monotone theory for dynamic system verification | Slides | This guest lecture is remote (zoom only) |
| L25 | 04/09 | Integral timed automata, reachability analysis (slides) | Ch 9 | HW3 out (due 04/27) |
| L26 | 04/11 | (Initialized) Rectangular Hybrid Automata (slides) | Ch 8, 9 | |
| L27 | 04/16 | Guest lecture (Soonho Kong): delta-satisfiability and dReal | This guest lecture is remote (zoom only) | |
| L28 | 04/18 | Abstractions, CEGAR (slides) | Ch 8 | HW4 out (Due 05/09) |
| L29 | 04/23 | Composition and compatibility of automata (slides) | Ch 5 | |
| L30 | 04/25 | Progress verification; stability of hybrid systems (slides) | Ch 10 | |
| L31 | 04/30 | Final presentations | ||
| L32 | 05/02 | Final presentations | ||
| 05/11 | Final Report Due |