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.

LectureDateTopicReadingsHomework
L101/16Introduction (slides) Ch1, Ch2
L201/18Modeling Computation, executions, invariance, reachability (slides) Ch2
L301/23Proofs of inductive invariance properties, Satisfiability problem. (slides) Ch 7.5HW1 out
(due 02/11)
L401/25Solving SAT problem, DPLL algorithm (slides) Ch 7.5
L501/30Satisfiability Modulo Theory (slides)Ch 7
L602/01SMT, Linear Real Arithmetic and Simplex (slides)Ch 7
L702/06Neural networks and machine learning systems; verification problem for ML-enabled systems (slides)
L802/08Verification as optimization problems; Integer programming and linear programming formulations for neural network verification (slides)
papers:
MILP formulation, LP formulation
L902/13Bound propagation algorithms for neural network verification (slides)papers:
CROWN
Convex-relaxation-barrier
L1002/15Branch-and-bound for neural network verification (slides)papers:
beta-CROWN
Branch-and-bound
L1102/20From algorithms to real-world NN verifiers; falsification, training of verifiable networks (slides)papers:
VNN-COMP
PGD attack
IBP training
HW2 out (due 03/10)
L1202/22Modeling physics, dynamical systems (slides)Ch 3
L1302/27Dynamical systems (Part II); discuss some ideas on class projects (slides)Ch 3
L1402/29Stability analysis of dynamical systems (slides)Ch 10.5
papers:
Lyapunov-stable neural-network control
Project proposal due 3/3
L1503/05Modeling cyberphysical systems. Hybrid automata (slides)Ch 4
L1603/07CPS Invariants; intro to CTL (slides)Ch 4, Ch 7
Spring break03/12No class
Spring break03/14No class
L1903/19intro to CTL; CTL model checking (slides)Ch 6
L2003/21CTL model checking, intro to timed automaton (slides)Ch 6, 9
L2103/26Mid-semester project reviewMidterm presentation slides due 3/25
L2203/28Mid-semester project reviewPresentation feedback due 3/29
L2304/02Guest lecture (Prof. Richard Y. Zhang): Semidefinite-programming-based neural network verificationPaper:
Low Rank SDP for NN verification
This guest lecture is in-person
L2404/04Guest lecture (Prof. Saber Jafarpour): Mixed-monotone theory for dynamic system verification
SlidesThis guest lecture is remote (zoom only)
L2504/09Integral timed automata, reachability analysis (slides)Ch 9HW3 out (due 04/27)
L2604/11(Initialized) Rectangular Hybrid Automata (slides)Ch 8, 9
L2704/16Guest lecture (Soonho Kong): delta-satisfiability and dRealThis guest lecture is remote (zoom only)
L2804/18Abstractions, CEGAR (slides)Ch 8HW4 out (Due 05/09)
L2904/23Composition and compatibility of automata (slides)Ch 5
L3004/25Progress verification; stability of hybrid systemsCh 10
L3104/30Final presentations
L3205/02Final presentations
05/11Final Report Due