15-424: Foundations of Cyber-Physical Systems (Sp'16)

Lecture notes and lecture videos, marked with (V), as well as further reading material will be made available on this page as the semester progresses. The supporting slides, marked with (S), are made available too, but only cover part of the lecture.


DateLecture NotesExtraDue
Tue 01/12Cyber-physical systems: introduction(V) (S) Ch 1
Thu 01/14Differential equations & domains(V) (S)  Ch 2.2,2.3, App.B
Fri 01/15Rec: ODE, FOL, prepAsst 0 
Tue 01/19Choice & control(V) Ch 2.2,2.3
Thu 01/21Safety & contracts(V) (S) Ch 2.2,2.3Lab 0 
Fri 01/22Rec: HP: Syntax, semantics, transitions, examples
Tue 01/26Dynamical systems & dynamic axioms(V) (SLICS'12
Thu 01/28Truth & proof(V) (S) Ch 2.5.2,App.AAsst 1 
Fri 01/29Rec: Manual proofs and tactical proofs in KeYmaera Xcode Beta 1 
Tue 02/02Control loops & invariants(V) (Scode Ch 2.5.2&4
Thu 02/04Events & responses(V) (Scode Lab 1 
Fri 02/05Rec: Did you prove what you meant to prove?
Tue 02/09Reactions & delays(V) (Scode 
Thu 02/11Differential equations & differential invariants(V) (Scode (Ch 3.5)Asst 2 
Fri 02/12Rec: Events to delayscode Beta 2 
Tue 02/16Differential equations & proofs(V) (S) (Ch 3.5)
Thu 02/18Ghosts & differential ghosts(V) (SLMCS'12Lab 2 
Fri 02/19Rec: Differential invariants, differential cutscode 
Tue 02/23Logical foundations & CPS(V) (SLICS'12Asst 3 
Thu 02/25Midterm
Fri 02/26Rec: Debugging models, understanding failed proofs, differential cutscode Beta 3 
Tue 03/01Differential invariants & proof theory(V) (SLMCS'12
Thu 03/03Verified models & verified runtime validation(V) (SFMSD'16Lab 3 
Fri 03/04Mid-semester break
Tue 03/08Spring break
Thu 03/10Spring break
Fri 03/11Spring break
Tue 03/15Hybrid systems & games(V) (STOCL'15
Thu 03/17Winning strategies & regions(V) (STOCL'15
Fri 03/18Rec: Game examples with fun and subtletyBeta 4 
Tue 03/22Winning & proving hybrid games(V) (STOCL'15Asst 4 
Thu 03/24Game proofs & separations(V) (STOCL'15
Fri 03/25Rec: Fun and proofs with gamesLab 4 
Tue 03/29Virtual substitution & real equations(V) (S) App.DWhite paper 
Thu 03/31Virtual substitution & real arithmetic(V) (SSturm
Fri 04/01Rec: Real arithmetic for real
Tue 04/05RecapAsst 5 
Thu 04/07Final exam
Fri 04/08Rec: Final posteriorProposal 
Tue 04/12Project day (no class)
Thu 04/14Spring Carnival
Fri 04/15Spring carnival
Tue 04/19Axioms & uniform substitutions(V) (SCADE'15
Thu 04/21Differential axioms & uniform substitutions(V) (SCADE'15
Fri 04/22Rec: Logical model-predictive control
Tue 04/26Model checking & reachability analysis(V) (SHBMC'17
Thu 04/28Distributed systems & hybrid systems(V) (SLMCS'12
Fri 04/29Rec: Prepare for Grand PrixProject Paper 
Thu 05/05CPS V&V Grand PrixSlides 
The lecture schedule is tentative!
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

Asst 00Preparation AssignmentFri 01/15
Lab 010Scavenger HuntcodeThu 01/21
Asst 160Introduction to Hybrid ProgramsThu 01/28
Beta 120Charging Station (Betabot)codeFri 01/29
Lab 170Charging Station (Veribot)codeThu 02/04
Asst 260Loops and ProofscodeThu 02/11
Beta 220Follow the Leader (Betabot)codeFri 02/12
Lab 280Follow the Leader (Veribot)codeThu 02/18
Asst 360Proofs, Diamonds, Differential InvariantsTue 02/23
Beta 320Robots on Racetracks (Betabot)codeFri 02/26
Lab 380Robots on Racetracks (Veribot)codeThu 03/03
Asst 460Differential Invariants and Cut-in DifferentiallyTue 03/22
Beta 420Static and Dynamic Obstacles (Betabot)codeFri 03/18
Lab 480Static and Dynamic Obstacles (Veribot)codeFri 03/25
Asst 560Play Around with Hybrid GamesTue 04/05
White paper20Star-lab White PaperTue 03/29
Proposal80Star-lab ProposalFri 04/08
Project100Star-lab Final ProjectFri 04/29
Paper100Term PaperFri 04/29
Slides0Slides and PresentationThu 05/05
Sum1000points 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.