This is a tentative schedule and is subject to change.
| Ln | Date | Topics | Notes |
|---|---|---|---|
| L1 | Tue 8/26 | Introduction, Discrete models Slides Video |
Jumpstart your project |
| L2 | Thu 8/28 | Invariance and reachability Slides Video |
HW1 out due 9/10 |
| L3 | Tue 9/02 | Inductive invariance; Satisfiability Slides Video |
|
| L4 | Thu 9/04 | Satisfiability, DPLL, SMT Slides Video | |
| L5 | Tue 9/09 | Satisfiability Modulo Theory Slides Video |
|
| T1 | Thu 9/11 | Z3 tutorial Slides Code |
|
| L6 | Tue 9/16 | SMT, LRA, Simplex Slides Video |
HW2 out |
| L7 | Thu 9/18 | Intro to Neural Network Verification Slides Video |
|
| L8 | Tue 9/23 | NN Verification (Part 2): LP, MILP formulations Slides Video |
|
| L9 | Thu 9/25 | NN Verification (Part 3): Interval & linear bound propagations Slides Video |
HW3 out |
| L10 | Tue 9/30 | Dynamical systems, examples, solutions, linear systems Slides Video |
|
| L11 | Thu 10/02 | Dynamical systems, Lyapunov theory Slides Video |
Proposal due |
| L12 | Tue 10/07 | Lypunov functions (Part 2) Slides Video |
|
| L13 | Thu 10/09 | Cyberphysical systems. Hybrid automata, Zeno CPS Invariants Slides Video |
|
| L14 | Tue 10/14 | Hybrid reachability, invariance, barriers and subtangents Slides Video |
|
| L15 | Thu 10/16 | Integral timed automata, abstraction, reachability Slides Video |
|
| M1 | Tue 10/21 | Midterm in class | |
| L16 | Thu 10/23 | Abstractions Slides Video |
HW5 out |
| P1 | Tue 10/28 | Project review part 1 Video |
|
| P2 | Thu 10/30 | Project review part 2 Video | |
| L17 | Tue 11/04 | Integral Timed to Rectangular Hybrid Automata Slides |
|
| L18 | Thu 11/06 | CEGAR: counterexample-guided abstraction refinement Notes | |
| L19 | Tue 11/11 | CTL model checking Slides |
|
| L21 | Thu 11/13 | No lecture | |
| L22 | Tue 11/18 | Undecidability, RHA, Counter machines Slides |
|
| L23 | Thu 11/20 | Compositions, I/O Automata, and Substitutivity Slides |
|
| Sun 11/30 | Fall break | ||
| P3 | Tue 12/02 | Project presentations | |
| P4 | Thu 12/04 | Project presentations | |
| P5 | Tue 12/09 | Project presentations | |
| Fri 12/12 | Final report |