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

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.


Tue 01/17Cyber-physical systems: introductionCh 1
Thu 01/19Differential equations & domains Ch 2.2,2.3, App.B
Fri 01/20Rec: ODE, FOL, prepAsst 0 
Tue 01/24Choice & controlCh 2.2,2.3
Thu 01/26Safety & contractsCh 2.2,2.3Lab 0 
Fri 01/27Rec: HP: Syntax, semantics, transitions, examples
Tue 01/31Dynamical systems & dynamic axioms LICS'12
Thu 02/02Truth & proofCh 2.5.2,App.AAsst 1 
Fri 02/03Rec: Manual proofs and tactical proofs in KeYmaera XBeta 1 
Tue 02/07Control loops & invariantsCh 2.5.2&4
Thu 02/09Events & responsesLab 1 
Fri 02/10Rec: Did you prove what you meant to prove?
Tue 02/14Reactions & delays
Thu 02/16Differential equations & differential invariants(Ch 3.5)Asst 2 
Fri 02/17Rec: Events to delaysBeta 2 
Tue 02/21Differential equations & proofs(Ch 3.5)
Thu 02/23Ghosts & differential ghosts LMCS'12 Lab 2 
Fri 02/24Rec: Differential invariants, differential cuts
Tue 02/28Logical foundations & CPS LICS'12 Asst 3 
Thu 03/02?Midterm?
Fri 03/03Rec: Debugging models, understanding failed proofs, differential cutsBeta 3 
Tue 03/07Differential invariants & proof theory LMCS'12
Thu 03/09Verified models & verified runtime validation FMSD'16 Lab 3 
Fri 03/10Mid-semester break
Tue 03/14Spring break
Thu 03/16Spring break
Fri 03/17Spring break
Tue 03/21Hybrid systems & games TOCL'15
Thu 03/23Winning strategies & regions TOCL'15
Fri 03/24Rec: Game examples with fun and subtletyBeta 4 
Tue 03/28Winning & proving hybrid games TOCL'15 Asst 4 
Thu 03/30Game proofs & separations TOCL'15
Fri 03/31Rec: Fun and proofs with gamesLab 4 
Tue 04/04Virtual substitution & real equationsApp.DWhite paper 
Thu 04/06Virtual substitution & real arithmetic
Fri 04/07Rec: Real arithmetic for real
Tue 04/11RecapAsst 5 
Thu 04/13Final exam
Fri 04/14Rec: Final posteriorProposal 
Tue 04/18TBD
Thu 04/20Spring Carnival
Fri 04/21Spring Carnival
Tue 04/25Axioms & uniform substitutions CADE'15
Thu 04/27Differential axioms & uniform substitutions CADE'15
Fri 04/28Rec: Logical model-predictive control
Tue 05/02Model checking & reachability analysis
Thu 05/04Distributed systems & hybrid systems LMCS'12
Fri 05/05Rec: Prepare for Grand PrixProject Paper 
Thu 05/11CPS 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/20
Lab 010Scavenger HuntThu 01/26
Asst 160Introduction to Hybrid ProgramsThu 02/02
Beta 120Charging Station (Betabot)Fri 02/03
Lab 170Charging Station (Veribot)Thu 02/09
Asst 260Loops and ProofsThu 02/16
Beta 220Follow the Leader (Betabot)Fri 02/17
Lab 280Follow the Leader (Veribot)Thu 02/23
Asst 360Proofs, Diamonds, Differential InvariantsTue 02/28
Beta 320Robots on Racetracks (Betabot)Fri 03/03
Lab 380Robots on Racetracks (Veribot)Thu 03/09
Asst 460Differential Invariants and Cut-in DifferentiallyTue 03/28
Beta 420Static and Dynamic Obstacles (Betabot)Fri 03/24
Lab 480Static and Dynamic Obstacles (Veribot)Fri 03/31
Asst 560Play Around with Hybrid GamesTue 04/11
White paper20Star-lab White PaperTue 04/04
Proposal80Star-lab ProposalFri 04/14
Project100Star-lab Final ProjectFri 05/05
Paper100Term PaperFri 05/05
Slides0Slides and PresentationThu 05/11
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.