Home
Administrivia
Overview
Schedule
Problem Sets
Resources
Archives
2012
| |
Date | Topic | Notes | Reading |
|---|---|---|---|---|
| L1 | Tue 08/26 | Motivation. Modeling Discrete Systems. Automata. HIOA Language. Invariants. | slides (.pdf) | Decidability & Complexity from [MSip96] |
| L2 | Thu 08/28 | Turing Machines, Languages and Decidability | Mahesh Viswanathan
slides (.pdf)
notes (.pdf) |
|
| L3 | Tue 09/02 | Complexity classes, P, NP, NL, PSPACE. NL Completeness of Reachability. | Mahesh Viswanathan
slides (.pdf)
notes (.pdf) |
|
| L4 | Thu 09/04 | Symbolic Reachability. Fix point characterization. | slides (.pdf) |
Chapter 3 [CGP00] |
| L5 | Tue 09/09 | An introduction to modern SMT solvers. Z3 tutorial. |
Sridhar Duggirala | References in slides |
| L6 | Thu 09/11 | Z3 tutorial continued | Read [TIOA06] Chapters 1-3 |
|
| L7 | Tue 09/16 | Hybrid automata. Executions, Examples. |
slides (.pdf) | Read [TIOA06] Chapters 1-3 |
| L8 | Thu 09/18 |
Reachability. Compositions of Hybrid Automata. |
slides (.pdf) | |
| L9 | Tue 09/23 | Properties of Compositions. Inductive invariants |
slides (.pdf) | |
| L10 | Thu 09/25 | Abstractions and Simulation | slides (.pdf) | Read [AD 94] |
| L11 | Tue 09/30 | Model Checking Timed Automata, Region Construction | slides (.pdf) | Read [Henz95] |
| L12 | Thu 10/02 | Timed to Rectangular Hybrid Automata | slides (.pdf) | [Henz95] |
| L13 | Tue 10/07 | Undecidable problems for timed and hybrid automata |
slides (.pdf) | |
| L14 | Thu 10/09 | Invariants and reachability of Linear HA, support functions, and SpaceEx | Sridhar slides (.pdf) |
SpaceEx website |
| L15 | Tue 10/14 | SpaceEx demo, PVS Introduction |
slides (.pdf) | PVS website |
| L16 | Thu 10/16 | PVS Tutorial | quick start notes (.pdf) | Stacks, MinProblem, TokenRing theories |
| L17 | Tue 10/21 | PVS part 2, Stability | slides (.pdf) | Refer to [DL03] Appendix A.Refer to [DL03] |
| L18 | Thu 10/23 | Stability verification, dynamical systems, Multiple Lyapunov functions | slides (.pdf) | |
| Tue 10/28 | No class |
|||
| L19 | Thu 10/30 | Simulation-based Verification | slides (.pdf) | C2E2 paper |
| L20 |
Tue 11/04 |
C2E2 tutorial | Sridhar | C2E2 user manual |
| L21 |
Thu 11/06 | CEGAR | ||
| L22 |
Tue 11/11 | Guest Lecture by James Lenz and Ashley Greer | ||
| L23 |
Thu 11/13 | Control law to embedded code: Giotto, Embedded machine and Logical Execution Time (LET) | slides (.pdf) | Giotto paper |
| L24 | Tue 11/18 | TBA |
||
| Thu 11/20 | Project presentations |
|||
| |
Tue 11/20 - 12/1 | Thanksgiving Break | |
|
| Tue 12/02 |
Project presentations | |||
| Thu 12/04 |
Project presentations | |||
| L26 | Tue 12/10 |