15-424: Logical Foundations of Cyber-Physical Systems (Fa'19)

Textbook chapters for the individual lectures are linked below, including supporting slides marked with (S) and supporting videos marked with (V). Neither slides nor videos always cover the full lecture. Flipped classroom material is marked with (N) but never covers the full lecture.


DateLecture NotesChExtraDue
Tue08/27Cyber-physical systems: introduction1(V) (S
Thu08/29Differential equations & domains2(V) (S) (N
Fri08/30Rec: Syntax, Semantics, FOL, ODEsAsst 0 
Tue09/03Choice & control3(V) (S
Thu09/05Safety & contracts4(V) (SLab 0 
Fri09/06Rec: Logic, programs, transition relations
Tue09/10Dynamical systems & dynamic axioms5(V) (Scode 
Thu09/12Truth & proof6(V) (S) (NAsst 1 
Fri09/13Rec: Common modeling errors and soundnesscode Beta 1 
Tue09/17Control loops & invariants7
Thu09/19Events & responses8Lab 1 
Fri09/20Rec: Eventful tactical KeYmaera X proofs
Tue09/24Reactions & delays9
Thu09/26Differential equations & differential invariants10Asst 2 
Fri09/27Rec: Time-triggered control and flying with differential invariantsBeta 2 
Tue10/01Differential equations & proofs11
Thu10/03Reviewing logical foundations & CPS Lab 2 
Fri10/04Rec: Differential invariants, differential cuts
Thu10/10Ghosts & differential ghosts12Asst 3 
Fri10/11Rec: ODE proofs and hybrid gamesCheck 3 
Tue10/15Differential invariants & proof theory13
Thu10/17Hybrid systems & games14Beta 3 
Fri10/18Free: Mid-semester break
Tue10/22Winning strategies & regions15
Thu10/24Winning & proving hybrid games16Lab 3 
Fri10/25Rec: TBDWhite paper 
Tue10/29Game proofs & separations17 TOCL'17
Thu10/31Final examAsst 4 
Fri11/01Rec: Fun and games with proofsBeta 4 
Tue11/05Hybrid games & differential games
Thu11/07Axioms & uniform substitutions18 JAR'17 Lab 4 
Fri11/08Rec: Convergence and uniform subst
Tue11/12Differential axioms & uniform substitutions18 JAR'17
Thu11/14Verified models & verified runtime validation19 FMSD'16 Asst 5 
Fri11/15Rec: KeYmaera X Tips and TricksProposal 
Tue11/19Virtual substitution & real equations20
Thu11/21Virtual substitution & real arithmetic21,
Fri11/22Rec: Real arithmetic for real
Tue11/26Free: Project day
Thu11/28Free: Thanksgiving
Fri11/29Free: Thanksgiving
Tue12/03CPS information-flow security and smartgrids LICS'18
Thu12/05Distributed systems & hybrid systems LMCS'12 Project 
Fri12/06Rec: Prepare for Grand PrixPaper 
Tue12/10CPS V&V Grand PrixSlides 

The lecture schedule is tentative!

The chapter numbers indicated above refer to the following textbook:

  1. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | doi | video | book | web | errata | abstract]

Logical Foundations of Cyber-Physical Systems

Lab Schedule

Asst 010Preparation AssignmentFri08/30
Lab 010Scavenger HuntcodeThu09/05
Asst 150Introduction to Hybrid ProgramsThu09/12
Beta 120Charging Station (Betabot)codeFri09/13
Lab 170Charging Station (Veribot)codeThu09/19
Asst 260Loops and ProofsThu09/26
Beta 220Follow the Leader (Betabot)Fri09/27
Lab 280Follow the Leader (Veribot)Thu10/03
Asst 360Proofs, Diamonds, Differential InvariantsThu10/10
Check 310Robots on Racetracks (Checkbot)Fri10/11
Beta 320Robots on Racetracks (Betabot)Thu10/17
Lab 370Robots on Racetracks (Veribot)Thu10/24
Asst 460Differential Invariants, Cuts, and Being GhostlyThu10/31
Beta 420Static and Dynamic Obstacles (Betabot)Fri11/01
Lab 480Static and Dynamic Obstacles (Veribot)Thu11/07
Asst 560Play Around with Hybrid GamesThu11/14
White paper20Star-lab White PaperFri10/25
Proposal80Star-lab ProposalFri11/15
Project100Star-lab Final ProjectThu12/05
Paper100Term PaperFri12/06
Slides0Slides and PresentationTue12/10
Sum1000points 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 at midnight). Theory assignments are due by midnight on the due day.

For an overview of the labs, see Labs & Assignments.