Lecture notes are linked below, including
lecture videos marked with (
▶)
and supporting slides marked with (
⊞).
Slides do not always cover the full lecture.
The lecture notes are significantly updated this semester, but the lecture videos are from
Spring 2016.
Schedule
| Date | Lecture Notes | Extra | Due |
|
| Tue | 01/17 | Cyber-physical systems: introduction | (▶) (⊞) | |
| Thu | 01/19 | Differential equations & domains | (▶) (⊞) | |
| Fri | 01/20 | Rec: ODE, FOL, prep | | Asst 0 |
|
| Tue | 01/24 | Choice & control | (▶) (⊞) | |
| Thu | 01/26 | Safety & contracts | (▶) (⊞) | Lab 0 |
| Fri | 01/27 | Rec: Programs, properties, transitions, and examples | code | |
|
| Tue | 01/31 | Dynamical systems & dynamic axioms | (▶) (⊞) code LICS'12 | |
| Thu | 02/02 | Truth & proof | (▶) (⊞) | Asst 1 |
| Fri | 02/03 | Rec: What is a proof and why? | code | Beta 1 |
|
| Tue | 02/07 | Control loops & invariants | (▶) (⊞) code | |
| Thu | 02/09 | Events & responses | (▶) (⊞) code | Lab 1 |
| Fri | 02/10 | Rec: Eventful tactical proofs in KeYmaera X | code | |
|
| Tue | 02/14 | Reactions & delays | (▶) (⊞) code | |
| Thu | 02/16 | Differential equations & differential invariants | (▶) (⊞) code | Asst 2 |
| Fri | 02/17 | Rec: Events to delays and flying with differential invariants | code | Beta 2 |
|
| Tue | 02/21 | Differential equations & proofs | (▶) (⊞) code | |
| Thu | 02/23 | Ghosts & differential ghosts | (▶) (⊞) code LMCS'12, extra | Lab 2 |
| Fri | 02/24 | Rec: Differential invariants, differential cuts, rolling down a hill | code | |
|
| Tue | 02/28 | Reviewing logical foundations & CPS | (▶) (⊞) LICS'12 | Asst 3 |
| Thu | 03/02 | Midterm | | |
| Fri | 03/03 | Rec: Proving differential equations with cuts and differential ghosts | code | Beta 3 |
|
| Tue | 03/07 | Differential invariants & proof theory | (▶) (⊞) LMCS'12 | |
| Thu | 03/09 | Verified models & verified runtime validation | (▶) (⊞) FMSD'16 | Lab 3 |
| Fri | 03/10 | Free: Mid-semester break | | |
|
| Tue | 03/14 | Free: Spring break | | |
| Thu | 03/16 | Free: Spring break | | |
| Fri | 03/17 | Free: Spring break | | |
|
| Tue | 03/21 | Hybrid systems & games | (▶) (⊞) TOCL'15 | |
| Thu | 03/23 | Winning strategies & regions | (▶) (⊞) TOCL'15 | Asst 4 |
| Fri | 03/24 | Rec: Game semantics, Geri's game, and Bus games | code | Beta 4 |
|
| Tue | 03/28 | Winning & proving hybrid games | (▶) (⊞) code TOCL'15 | |
| Thu | 03/30 | Game proofs & separations | (▶) (⊞) TOCL'15 TOCL'17 | Lab 4 |
| Fri | 03/31 | Rec: Fun and games with proofs | code | White paper |
|
| Tue | 04/04 | Axioms & uniform substitutions | (▶) (⊞) JAR'17 | |
| Thu | 04/06 | Differential axioms & uniform substitutions | (▶) (⊞) JAR'17 | Asst 5 |
| Fri | 04/07 | Rec: Uniform subst and review | | |
|
| Tue | 04/11 | Recap | | |
| Thu | 04/13 | Final exam | | |
| Fri | 04/14 | Rec: Project modeling, baseball proving, decomposing models, logical model-predictive control | code | |
|
| Tue | 04/18 | Optional: Safety & CPS Implementations | | Proposal |
| Thu | 04/20 | Free: Spring Carnival | | |
| Fri | 04/21 | Free: Spring Carnival | | |
|
| Tue | 04/25 | Virtual substitution & real equations | (▶) (⊞) | |
| Thu | 04/27 | Virtual substitution & real arithmetic | (▶) (⊞) , extra | |
| Fri | 04/28 | Rec: Real arithmetic for real | code | |
|
| Tue | 05/02 | Distributed systems & hybrid systems | (▶) (⊞) LMCS'12 | |
| Thu | 05/04 | Hybrid systems & complete proofs | (⊞) LICS'12 | Project |
| Fri | 05/05 | Rec: Prepare for Grand Prix | | Paper |
|
| Thu | 05/11 | CPS V&V Grand Prix | | Slides |
The lecture schedule is tentative!
Lab Schedule
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 at midnight).
Theory assignments are due by midnight on the due day.
For an overview of the labs, see Labs & Assignments.
