Home
Administrivia
Overview
Schedule
Problem Sets
Resources
Archives
2012
2014
| |
Date | Topic | Notes | Reading |
|---|---|---|---|---|
| L1 | Tue 01/19 | Motivation. Modeling Discrete Systems. Automata. HIOA Language. Invariants. | slides (.pdf) | Decidability & Complexity from [MSip96] |
| L2 | Thu 01/21 | Turing Machines, Languages and Decidability | slides (.pdf) | |
| L3 | Tue 01/26 | Complexity classes, P, NP, NL, PSPACE. NL Completeness of Reachability. | slides (.pdf) | |
| L4 | Thu 01/28 | Symbolic Reachability. Fix point characterization. | slides (.pdf) |
Chapter 3 [CGP00] |
| L5 | Tue 02/02 | An introduction to modern SMT solvers. Z3 tutorial. |
slides (.pdf) | References in slides |
| L6 | Thu 02/04 | Z3 tutorial continued | Read [TIOA06] Chapters 1-3 |
|
| L7 | Tue 02/09 | Hybrid automata. Executions, Examples. |
slides (.pdf) | Read [TIOA06] Chapters 1-3 |
| L8 | Thu 02/11 |
Reachability. Examples. |
slides (.pdf) | |
| L9 | Tue 02/16 | Executions, reachability, inductive invariants |
slides (.pdf) | |
| L10 | Thu 02/18 | Compositions, abstractions and Simulation | slides (.pdf) | |
| L11 | Tue 02/23 | PVS Tutorial: Intro | PVS website |
|
| L12 | Thu 02/25 | PVS Tutorial: Language | slides (.pdf) | Stacks, MinProblem, TokenRing theories |
| L13 | Tue 03/01 | PVS Tutorial: Prover |
slides (.pdf) | |
| L14 | Thu 03/03 | Abstraction and simulation relations; weak, strong, time-abstract | Read [AD 94] | |
| L15 | Tue 03/08 | Timed automata
Automata; |
slides (.pdf) | |
| L16 | Thu 03/10 | Timed to to rectangular hybrid automata | slides (.pdf) | [Henz95] |
| Tue 03/15 | No class | SpaceEx website | ||
| Thu 03/17 | Project review | |||
| Tue 03/22-24 | Spring break |
|||
| L17 | Tue 03/29 | Undecidable problems for timed and hybrid automata | slides (.pdf) | |
| L18 |
Thu 03/31 | Stability verification, dynamical systems, Lyapunov functions | slides (.pdf) | |
| L19 |
Tue 04/05 | Stability verification, hybrid systems, Multiple Lyapunov functions, dwell time | slides (.pdf) | |
| L20 |
Thu 04/07 | Temporal logic and controller synthesis | slides (.pdf) | |
| 04/12-14 | No class | |||
| L21 |
Tue 04/19 | Simulation-based verification: C2E2 Tutorial 1 | Guest lecture by Chuchu Fan |
|
| L22 | Thu 04/21 | TBA: Guest Lecture by James Lenz and Ashley Greer |
||
| L23 | Tue 04/26 | C2E2 Tutorial 2 |
||
| P1 | Thu 04/28 | Project presentations 1,2,3 | ||
| P2 | May 05/03 | Project presentations 4,5,6 |