Textbook chapters for the individual lectures are linked below,
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.
(▶) = videos (⊞) = slides
Schedule
| Date | Lecture Notes | Ch | Extra | Due |
|
| Tue | 08/31 | Cyber-physical systems: introduction | 1 | (▶) (⊞) | |
| Thu | 09/02 | Differential equations & domains | 2 | (▶) (⊞) | |
| Fri | 09/03 | Rec: Syntax, Semantics, FOL, ODEs | | | Asst 1 |
|
| Tue | 09/07 | Choice & control | 3 | (▶) (⊞) | |
| Thu | 09/09 | Safety & contracts | 4 | (▶) (⊞) | |
| Fri | 09/10 | Rec: Logic, programs, transition relations | | code | Lab 0 |
|
| Tue | 09/14 | Dynamical systems & dynamic axioms | 5 | (▶) (⊞) code | Beta 1 |
| Thu | 09/16 | Truth & proof | 6 | (▶) (⊞) | |
| Fri | 09/17 | Rec: Common modeling errors and soundness | | code | |
|
| Tue | 09/21 | Control loops & invariants | 7 | (▶) (⊞) code | Lab 1 |
| Thu | 09/23 | Events & responses | 8 | (▶) (⊞) code | |
| Fri | 09/24 | Rec: Eventful tactical KeYmaera X proofs | | code | Asst 2 |
|
| Tue | 09/28 | Reactions & delays | 9 | (▶) (⊞) code | Beta 2 |
| Thu | 09/30 | Differential equations & differential invariants | 10 | (▶) (⊞) code | |
| Fri | 10/01 | Rec: Time-triggered control, differentials, differential invariant terms | | code | |
|
| Tue | 10/05 | Differential equations & proofs | 11 | (▶) (⊞) code | Lab 2 |
| Thu | 10/07 | Reviewing logical foundations & CPS | | | |
| Fri | 10/08 | Rec: Differential invariants, differential cuts | | code | Asst 3 |
|
| Tue | 10/12 | Midterm I | | | |
| Thu | 10/14 | Free: Mid-Semester Break | | | |
| Fri | 10/15 | Free: Mid-Semester Break | | | |
|
| Tue | 10/19 | Hybrid systems & games | 14 | (▶) (⊞) | Beta 3 |
| Thu | 10/21 | Winning strategies & regions | 15 | (▶) (⊞) | Whitepap. |
| Fri | 10/22 | Rec: Game semantics, Geri's game, bus games | | | |
|
| Tue | 10/26 | Winning & proving hybrid games | 16 | (▶) (⊞) code | Lab 3 |
| Thu | 10/28 | Ghosts & differential ghosts | 12 | (▶) (⊞) code | |
| Fri | 10/29 | Rec: Game proofs and go with ghosts | | | |
|
| Tue | 11/02 | Game proofs & separations | 17 | (▶) (⊞) TOCL'17 | Beta 4 |
| Thu | 11/04 | Axioms & uniform substitutions | 18 | (▶) (⊞) more | |
| Fri | 11/05 | Free: Day for Community Engagement | | | |
|
| Tue | 11/09 | Exam review | | (▶) | Lab 4 |
| Thu | 11/11 | Midterm II | | | |
| Fri | 11/12 | Rec: Modeling and proving with diamonds | | code | |
|
| Tue | 11/16 | Verified models & verified runtime validation | 19 | (▶) (⊞) | Proposal |
| Thu | 11/18 | Differential equations & completeness | | (▶) (⊞) JACM'20 | |
| Fri | 11/19 | Rec: Validation, Simulation and Synthesis | | | |
|
| Tue | 11/23 | Free: Project day | | | |
| Thu | 11/25 | Free: Thanksgiving | | | |
| Fri | 11/26 | Free: Thanksgiving | | | |
|
| Tue | 11/30 | Virtual substitution & real equations | 20 | (▶) (⊞) FM'21 | |
| Thu | 12/02 | Virtual substitution & real arithmetic | 21 | (▶) (⊞)
CH,
extra | Project |
| Fri | 12/03 | Rec: Wrestling with real arithmetic | | code | Paper |
|
| Fri | 12/10 | 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.
| Points | Assignment | | Due |
| Asst 1 | 0 | Preparation Assignment | | Fri | 09/03 |
| Lab 0 | 10 | Scavenger Hunt | | Fri | 09/10 |
| Beta 1 | 15 | Charging Station (Betabot) | | Tue | 09/14 |
| Lab 1 | 75 | Charging Station (Veribot) | | Tue | 09/21 |
| Asst 2 | 40 | Loops and Proofs | | Fri | 09/24 |
| Beta 2 | 20 | Follow the Leader (Betabot) | | Tue | 09/28 |
| Lab 2 | 80 | Follow the Leader (Veribot) | | Tue | 10/05 |
| Asst 3 | 40 | Proofs, Differential Invariants | | Fri | 10/08 |
| Beta 3 | 30 | Robots on Racetracks (Betabot) | | Tue | 10/19 |
| Lab 3 | 70 | Robots on Racetracks (Veribot) | | Tue | 10/26 |
| Beta 4 | 20 | Static and Dynamic Obstacles (Betabot) | | Tue | 11/02 |
| Lab 4 | 80 | Static and Dynamic Obstacles (Veribot) | | Tue | 11/09 |
| Whitepap. | 20 | Star-lab White Paper | | Thu | 10/21 |
| Proposal | 80 | Star-lab Proposal | | Tue | 11/16 |
| Project | 100 | Star-lab Final Project | | Thu | 12/02 |
| Paper | 100 | Term Paper | | Fri | 12/03 |
| Slides | 0 | Slides and Presentation | | Fri | 12/10 |
| Sum | 780 | points listed |
The Lab and Assignment Schedule is tentative!
Labs have a due date and time for Betabots and a different due date and time for Veribots.
Theory assignments are due on the due day.
More specific due times are listed on Diderot.
For an overview of the labs, see Labs & Assignments.
