Textbook chapters for the individual lectures are linked below, including supporting slides marked with (
⊞) and supporting
videos marked with (
▶).
Neither slides nor videos always cover the full lecture.
Flipped classroom material is marked with (
N) but never covers the full lecture.
(▶) = videos (⊞) = slides
(N) = flipped
Schedule
| Date | Lecture Notes | Ch | Extra | Due |
|
| Tue | 09/01 | Cyber-physical systems: introduction | 1 | (▶) (⊞) | |
| Thu | 09/03 | Differential equations & domains | 2 | (▶) (⊞) | |
| Fri | 09/04 | Rec: Syntax, Semantics, FOL, ODEs | | | Asst 0 |
|
| Tue | 09/08 | Choice & control | 3 | (▶) (⊞) | |
| Thu | 09/10 | Safety & contracts | 4 | (▶) (⊞) | Lab 0 |
| Fri | 09/11 | Rec: Logic, programs, transition relations | | (⊞) | |
|
| Tue | 09/15 | Dynamical systems & dynamic axioms | 5 | (▶) (⊞) code | |
| Thu | 09/17 | Truth & proof | 6 | (▶) (⊞) | Asst 1 |
| Fri | 09/18 | Rec: Common modeling errors and soundness | | (⊞) code | Beta 1 |
|
| Tue | 09/22 | Control loops & invariants | 7 | (▶) (⊞) code | |
| Thu | 09/24 | Events & responses | 8 | (▶) (⊞) code | Lab 1 |
| Fri | 09/25 | Rec: Eventful tactical KeYmaera X proofs | | (⊞) code | |
|
| Tue | 09/29 | Reactions & delays | 9 | (▶) (⊞) code | |
| Thu | 10/01 | Differential equations & differential invariants | 10 | (▶) (⊞) code | Asst 2 |
| Fri | 10/02 | Rec: Time-triggered control, differentials, differential invariant terms | | (⊞) code | Beta 2 |
|
| Tue | 10/06 | Differential equations & proofs | 11 | (▶) (⊞) code | |
| Thu | 10/08 | Ghosts & differential ghosts | 12 | (▶) (⊞) code | Lab 2 |
| Fri | 10/09 | Rec: Differential invariants, differential cuts, differential ghosts | | code more | |
|
| Tue | 10/13 | Reviewing logical foundations & CPS | | | Asst 3 |
| Thu | 10/15 | Midterm I | | | |
| Fri | 10/16 | Free: Day for Community Engagement | | | |
|
| Tue | 10/20 | Hybrid systems & games | 14 | (▶) (⊞) | Beta 3 |
| Thu | 10/22 | Winning strategies & regions | 15 | (▶) (⊞) | White paper |
| Fri | 10/23 | Free: Mid-semester break | | | |
|
| Tue | 10/27 | Winning & proving hybrid games | 16 | (▶) (⊞) code | Lab 3 |
| Thu | 10/29 | Rec: Game semantics, Geri's game, bus games, proved games | | (⊞) | |
| Fri | 10/30 | Axioms & uniform substitutions | 18 | (▶) (⊞) | |
|
| Tue | 11/03 | Game proofs & separations | 17 | (▶) (⊞) TOCL'17 | Asst 4 |
| Thu | 11/05 | Differential axioms & uniform substitutions | 18 | (▶) (⊞) JAR'17 | Beta 4 |
| Fri | 11/06 | Rec: Convergence and uniform subst | | (⊞) code | |
|
| Tue | 11/10 | Exam review | | (▶) | Lab 4 |
| Thu | 11/12 | Midterm II | | | |
| Fri | 11/13 | Rec: Modeling and proving with diamonds | | (⊞) code | |
|
| Tue | 11/17 | Verified models & verified runtime validation | 19 | (▶) (⊞) | |
| Thu | 11/19 | Differential equations & completeness | | (▶) (⊞) JACM'20 | |
| Fri | 11/20 | Rec: Synthesis, Simulation, and Validation | | (⊞) | Proposal |
|
| Tue | 11/24 | Free: Project day | | | |
| Thu | 11/26 | Free: Thanksgiving | | | |
| Fri | 11/27 | Free: Thanksgiving | | | |
|
| Tue | 12/01 | Virtual substitution & real equations | 20 | (▶) (⊞) | |
| Thu | 12/03 | Virtual substitution & real arithmetic | 21 | (▶) (⊞) ,
extra | |
| Fri | 12/04 | Rec: Wrestling with real arithmetic | | (⊞) code | |
|
| Tue | 12/08 | Hybrid systems & continuous completeness | | (⊞) LICS'12,JAR'17 | |
| Thu | 12/10 | Hybrid systems & discrete completeness | | (⊞) LICS'12,JAR'17 | Project |
| Fri | 12/11 | Distributed systems & hybrid systems | | (⊞) LMCS'12 | Paper |
|
| Fri | 12/18 | CPS V&V Grand Prix | | | Slides |
The lecture schedule is tentative!
The chapter numbers indicated above refer to the following textbook:
Lab Schedule
Assignments, labs, and quizzes are released on Diderot (or see previous years)
| Points | Assignment | | Due |
| Asst 0 | 0 | Preparation Assignment | | Fri | 09/04 |
| Lab 0 | 10 | Scavenger Hunt | | Thu | 09/10 |
| Asst 1 | 40 | Introduction to Hybrid Programs | | Thu | 09/17 |
| Beta 1 | 15 | Charging Station (Betabot) | | Fri | 09/18 |
| Lab 1 | 75 | Charging Station (Veribot) | | Thu | 09/24 |
| Asst 2 | 40 | Loops and Proofs | | Thu | 10/01 |
| Beta 2 | 20 | Follow the Leader (Betabot) | | Fri | 10/02 |
| Lab 2 | 80 | Follow the Leader (Veribot) | | Thu | 10/08 |
| Asst 3 | 40 | Proofs, Differential Invariants | | Tue | 10/13 |
| Beta 3 | 30 | Robots on Racetracks (Betabot) | | Tue | 10/20 |
| Lab 3 | 70 | Robots on Racetracks (Veribot) | | Tue | 10/27 |
| Asst 4 | 40 | ODEs, Ghosts, and Games | | Tue | 11/03 |
| Beta 4 | 20 | Static and Dynamic Obstacles (Betabot) | | Thu | 11/05 |
| Lab 4 | 80 | Static and Dynamic Obstacles (Veribot) | | Tue | 11/10 |
| White paper | 20 | Star-lab White Paper | | Thu | 10/22 |
| Proposal | 80 | Star-lab Proposal | | Fri | 11/20 |
| Project | 100 | Star-lab Final Project | | Thu | 12/10 |
| Paper | 100 | Term Paper | | Fri | 12/11 |
| Slides | 0 | Slides and Presentation | | Fri | 12/18 |
| Sum | 860 | points listed |
The Lab and Assignment Schedule is tentative!
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 before midnight).
Theory assignments are due before midnight on the due day.
For an overview of the labs, see Labs & Assignments.
