Home
Administrivia
Overview
Schedule
Problem Sets
Resources
| |
Date | Topic | Notes (Scribe) | Reading |
|---|---|---|---|---|
| L1 | Tue 09/04 | Motivation, examples of systems and propositional logic, proofs | .pptx
.pdf |
Decidability & Complexity from [MSip96] |
| L2 | Thu 09/06 | Predicate Logic, Intro to hybrid automata | .pptx
.pdf marked .pdf |
Chapters 3 & 4 from [TIOA06] |
| L3 | Tue 09/11 | Executions, Invariance, Reachability | .pptx marked .pdf |
Chapters 3 & 4 from [TIOA06] |
| L4 | Thu 09/13 | Abstractions and Simulation Relations | .pptx
(Debjit) marked .pdf |
|
| L5 | Tue 09/18 | Composition and Substitutivity |
.pptx marked .pptx |
Project proposals due. HW1 posted. |
| L6 | Thu 09/20 | Substitutivity (cont.). PVS Tutorial Part I. | .pptx marked .pptx |
|
| L7 | Tue 09/25 | PVS Tutorial Part II |
.pdf |
PVS Theories for Stacks
and MinProblem . |
| L8 | Thu 09/27 | PVS Prover Tutorial |
Same as above |
|
| L9 | Tue 10/02 | Model Checking Timed Automata, Region Construction | .pptx
(Yu) |
Read [AD 94] HW1 due |
| |
Thu 10/04 | Allerton Session on CPS Verification | ||
| L10 | Tue 10/09 | Timed to Rectangular Hybrid
Automata |
.pptx
(Adel) |
Read [Henz95] |
| L11 | Thu 10/11 | Safety Verification of Linear HA, support functions, and SpaceEx | Guest Lecture by P. Sridhar Duggirala |
|
| L12 | Tue 10/16 | Undecidability of non-initialized rectangular HA | .pdf
(notes) |
[Henz95] |
| L13 | Thu 10/18 | Modern SMT solvers. Z3 Tutorial,Symbolic model checking | .pdf .zip (examples) |
Guest Lecture by Taylor Johnson |
| L14 | Tue 10/23 | Discussion of HW1 + Stability |
class notes
|
|
| L15 | Thu 10/25 | Stability of Nonlinear
Systems |
notes class notes |
Refer to [DL03] Appendix A. |
| L16 | Tue 10/30 | Stability verification: Multiple Lyapunov functions | class notes | Refer to [DL03] |
| L17 | Thu 11/01 | Stability verification: slow switching, with delays | class notes | |
| L18 | Tue 11/06 | Introduction Abstract
Interpretation |
.pptx
|
|
| L19 | Thu 11/08 | Invariant synthesis for hybrid systems | ||
| L20 |
Tue 11/13 |
CEGAR | .pdf |
|
| L21 |
Thu 11/15 | Controller synthesis from temporal logic | .pptx |
|
| |
Tue 11/20 | Thanksgiving
break |
||
| |
Thu 11/22 | Thanksgiving break | ||
| L22 | Tue 11/27 | Time-triggered implementation of hybrid systems (Giotto) | ||
| |
Thu 11/29 | No class |
||
| |
Tue 12/04 | No class | |
|
| Thu 12/06 |
No class | |||
| L23 | Tue 12/11 |
Course wrap-up and first project presentation | ||
| Sun 12/16 |
Course Project Presentations |
| |
Title |
Participants |
Slides |
Talk |
|---|---|---|---|---|
| P1 | Verification of nonlinear hybrid systems | Adel and Ranato | .pdf |
Tuesday |
| P2 | Reformulation of
a Result on Networks of Hybrid Systems |
Sean Shahkarami |
.pdf |
Dec 16 |
| P3 | A Case study on
Verification of a Helicopter Model |
Raymond Essick |
.pdf |
Dec 16 |
| P4 | Bounded Verification on Nonlinear HS from
Simulink/Stateflow Models |
Zhenqi Huang |
.pdf |
Dec 16 |
| P5 | Combining
Theorem-proving & model-checking for Verifying the
SATS |
Dileep Kini |
.pdf |
Dec 16 |
| P6 | Checking for Patent Similarities using SMT solvers |
Koushik Roy |
Dec 16 | |
| P7 | Verification of
Power Electoric Converters |
Shamina Hossain |
.pdf |
Dec 16 |
| P8 | Atmel Micro-controller and AVR ISA Platform Level
Verification |
Joseph Girotti |
.pdf |
Dec 16 |
| P9 | Modeling and
Analysis of Distributed Robotic Systems |
Adam Zimmerman | .pdf |
Dec 16 |
| P10 | Safe Control of Distributed Cyber-Physical
Systems |
Fardin Abdi Taghi | .pdf |
Dec 16 |
| P11 | Translating
Simulink/Stateflow models to Hybrid automata |
Debjit Pal | .pdf |
Dec 16 |
| P13 | Decidability of
Almost Rectangular Hybrid Systems |
Nima Roohi |
.pdf |
Dec 16 |