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/21 | Introduction (slides) | Ch1, Ch2 | |
| L2 | 01/23 | Modeling Computation, executions, invariance, reachability (slides) | Ch2 | |
| L3 | 01/28 | Proofs of inductive invariance properties, Satisfiability problem (slides) | Ch 7.5 | |
| L4 | 01/30 | Solving SAT problem, DPLL algorithm, NeuroSAT (slides) | Ch 7.5 | |
| L5 | 02/04 | Satisfiability Modulo Theory (slides) | Ch 7 | HW 1 is out. (Due: 02/17) |
| L6 | 02/06 | Past Students Research Project Presentations (Chenxi Ji, Jiaxin Wan, Mani Jha, Jorge Chavez, Duo Zhou) | Ask them questions about class project! | |
| L7 | 02/11 | SMT, Linear Real Arithmetic and Simplex (slides) | Ch 7 | |
| L8 | 02/13 | Neural networks and machine learning systems; verification problem for ML-enabled systems (slides) | ||
| L9 | 02/18 | Verification as optimization problems; Integer programming and linear programming formulations for neural network verification (slides) | papers: MILP formulation LP formulation | |
| L10 | 02/20 | Bound propagation algorithms for neural network verification (slides) | papers: CROWN Convex-relaxation-barrier | |
| L11 | 02/25 | Branch-and-bound for neural network verification (slides) | papers: beta-CROWN Branch-and-bound | |
| L12 | 02/27 | Guest lecture: Prof. Haoze Wu (Zoom) | Lecture On Zoom | Project proposal due 3/5 |
| L13 | 03/04 | From algorithms to real-world NN verifiers; falsification, training of verifiable networks (slides) | papers: VNN-COMP PGD attack IBP training | |
| L14 | 03/06 | Modeling physics, dynamical systems (Part I: concepts) (slides) | Ch 3 | |
| L15 | 03/11 | Dynamical systems (Part II: linear systems) (slides) | Ch 3 | |
| L16 | 03/13 | Stability analysis of dynamical systems (slides) | Ch 10.5 papers: Lyapunov-stable neural-network control | HW 2 due 3/17 |
| Spring break | 03/18 | No class (Spring break) | ||
| Spring break | 03/20 | No class (Spring break) | ||
| L19 | 03/25 | Mid-semester project review | Midterm presentation slides due 3/24 | |
| L20 | 03/27 | Mid-semester project review | ||
| L21 | 04/01 | Modeling cyber-physical systems. Hybrid automata (slides) | Ch 4 | |
| L22 | 04/03 | CPS Invariants; intro to CTL (slides) | Ch 4, Ch 7 | |
| L23 | 04/08 | Intro to CTL; CTL model checking (slides) | Ch 6 | |
| L24 | 04/10 | Intro to timed automaton and integral timed automaton; reachability (slides) | Ch 6, 9 | |
| L25 | 04/15 | Reachability analysis of timed automaton and (Initialized) Rectangular Hybrid Automata (slides) | Ch 8, 9 | |
| L26 | 04/17 | Abstractions, CEGAR (slides) | Ch 8 | HW3 due 4/22 |
| L27 | 04/22 | Composition and compatibility of automata (slides) | Ch 5 | |
| L28 | 04/24 | Progress verification; stability of hybrid systems (slides) | Ch 10 | |
| L29 | 04/29 | Final presentations | All presentation slides due on 4/29 at 11 am (hard) | |
| L30 | 05/01 | Final presentations | ||
| L31 | 05/06 | Final Project Office Hour (come to the classroom for your questions) | HW4 due 5/10 | |
| 05/18 | Final Report Due | Final report due 5/18 |