Schedule
| Date | Lecture Notes | Extra | Due | |
|---|---|---|---|---|
| Tue | 01/12 | Cyber-physical systems: introduction | (V) (S) Ch 1 | |
| Thu | 01/14 | Differential equations & domains | (V) (S) Ch 2.2,2.3, App.B | |
| Fri | 01/15 | Rec: ODE, FOL, prep | Asst 0 | |
| Tue | 01/19 | Choice & control | (V) Ch 2.2,2.3 | |
| Thu | 01/21 | Safety & contracts | (V) (S) Ch 2.2,2.3 | Lab 0 |
| Fri | 01/22 | Rec: HP: Syntax, semantics, transitions, examples | ||
| Tue | 01/26 | Dynamical systems & dynamic axioms | (V) (S) LICS'12 | |
| Thu | 01/28 | Truth & proof | (V) (S) Ch 2.5.2,App.A | Asst 1 |
| Fri | 01/29 | Rec: Manual proofs and tactical proofs in KeYmaera X | code | Beta 1 |
| Tue | 02/02 | Control loops & invariants | (V) (S) code Ch 2.5.2&4 | |
| Thu | 02/04 | Events & responses | (V) (S) code | Lab 1 |
| Fri | 02/05 | Rec: Did you prove what you meant to prove? | ||
| Tue | 02/09 | Reactions & delays | (V) (S) code | |
| Thu | 02/11 | Differential equations & differential invariants | (V) (S) code (Ch 3.5) | Asst 2 |
| Fri | 02/12 | Rec: Events to delays | code | Beta 2 |
| Tue | 02/16 | Differential equations & proofs | (V) (S) (Ch 3.5) | |
| Thu | 02/18 | Ghosts & differential ghosts | (V) (S) LMCS'12 | Lab 2 |
| Fri | 02/19 | Rec: Differential invariants, differential cuts | code | |
| Tue | 02/23 | Logical foundations & CPS | (V) (S) LICS'12 | Asst 3 |
| Thu | 02/25 | Midterm | ||
| Fri | 02/26 | Rec: Debugging models, understanding failed proofs, differential cuts | code | Beta 3 |
| Tue | 03/01 | Differential invariants & proof theory | (V) (S) LMCS'12 | |
| Thu | 03/03 | Verified models & verified runtime validation | (V) (S) FMSD'16 | Lab 3 |
| Fri | 03/04 | Free: Mid-semester break | ||
| Tue | 03/08 | Free: Spring break | ||
| Thu | 03/10 | Free: Spring break | ||
| Fri | 03/11 | Free: Spring break | ||
| Tue | 03/15 | Hybrid systems & games | (V) (S) TOCL'15 | |
| Thu | 03/17 | Winning strategies & regions | (V) (S) TOCL'15 | |
| Fri | 03/18 | Rec: Game examples with fun and subtlety | Beta 4 | |
| Tue | 03/22 | Winning & proving hybrid games | (V) (S) TOCL'15 | Asst 4 |
| Thu | 03/24 | Game proofs & separations | (V) (S) TOCL'15 | |
| Fri | 03/25 | Rec: Fun and proofs with games | Lab 4 | |
| Tue | 03/29 | Virtual substitution & real equations | (V) (S) App.D | White paper |
| Thu | 03/31 | Virtual substitution & real arithmetic | (V) (S) Sturm | |
| Fri | 04/01 | Rec: Real arithmetic for real | ||
| Tue | 04/05 | Recap | Asst 5 | |
| Thu | 04/07 | Final exam | ||
| Fri | 04/08 | Rec: Final posterior | Proposal | |
| Tue | 04/12 | Free: Project day (no class) | ||
| Thu | 04/14 | Free: Spring Carnival | ||
| Fri | 04/15 | Free: Spring carnival | ||
| Tue | 04/19 | Axioms & uniform substitutions | (V) (S) CADE-25 | |
| Thu | 04/21 | Differential axioms & uniform substitutions | (V) (S) CADE-25 | |
| Fri | 04/22 | Rec: Logical model-predictive control | ||
| Tue | 04/26 | Model checking & reachability analysis | (V) (S) HBMC'17 | |
| Thu | 04/28 | Distributed systems & hybrid systems | (V) (S) LMCS'12 | |
| Fri | 04/29 | Rec: Prepare for Grand Prix | Project Paper | |
| Thu | 05/05 | CPS V&V Grand Prix | Slides | |
Reading: The chapters Ch i.j and App i for further reading refer to chapters in the textbook in addition to the lecture notes.
Lab Schedule
| Points | Assignment | Due | |||
|---|---|---|---|---|---|
| Asst 0 | 0 | Preparation Assignment | Fri | 01/15 | |
| Lab 0 | 10 | Scavenger Hunt | code | Thu | 01/21 |
| Asst 1 | 60 | Introduction to Hybrid Programs | Thu | 01/28 | |
| Beta 1 | 20 | Charging Station (Betabot) | code | Fri | 01/29 |
| Lab 1 | 70 | Charging Station (Veribot) | code | Thu | 02/04 |
| Asst 2 | 60 | Loops and Proofs | code | Thu | 02/11 |
| Beta 2 | 20 | Follow the Leader (Betabot) | code | Fri | 02/12 |
| Lab 2 | 80 | Follow the Leader (Veribot) | code | Thu | 02/18 |
| Asst 3 | 60 | Proofs, Diamonds, Differential Invariants | Tue | 02/23 | |
| Beta 3 | 20 | Robots on Racetracks (Betabot) | code | Fri | 02/26 |
| Lab 3 | 80 | Robots on Racetracks (Veribot) | code | Thu | 03/03 |
| Asst 4 | 60 | Differential Invariants and Cut-in Differentially | Tue | 03/22 | |
| Beta 4 | 20 | Static and Dynamic Obstacles (Betabot) | code | Fri | 03/18 |
| Lab 4 | 80 | Static and Dynamic Obstacles (Veribot) | code | Fri | 03/25 |
| Asst 5 | 60 | Play Around with Hybrid Games | Tue | 04/05 | |
| White paper | 20 | Star-lab White Paper | Tue | 03/29 | |
| Proposal | 80 | Star-lab Proposal | Fri | 04/08 | |
| Project | 100 | Star-lab Final Project | Fri | 04/29 | |
| Paper | 100 | Term Paper | Fri | 04/29 | |
| Slides | 0 | Slides and Presentation | Thu | 05/05 | |
| Sum | 1000 | points listed | |||
The Lab and Assignment Schedule is tentative!
Theory assignments and Betabot lab assignments are due at start of lecture/recitation on the due day.
Veribot lab assignments are due at 22:00 on the due day.
Labs have a due date and time for Betabots (due at start of lecture/recitation) and a different due date and time for Veribots (due at 22:00).
For an overview of the labs, see Labs & Assignments.