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

Lecture notes are linked below, including lecture videos marked with (V) and supporting slides marked with (S). Slides do not always cover the full lecture. The lecture notes are significantly updated this semester, but the lecture videos are from Spring 2016.


DateLecture NotesChExtraDue
Tue08/28Cyber-physical systems: introduction1(S
Thu08/30Differential equations & domains2(S
Fri08/31Rec: ODE, FOL, prepAsst 0 
Tue09/04Choice & control3(S
Thu09/06Safety & contracts4(SLab 0 
Fri09/07Rec: Programs, properties, transitions, and examples
Tue09/11Dynamical systems & dynamic axioms5(Scode 
Thu09/13Truth & proof6(SAsst 1 
Fri09/14Rec: What is a proof and why?code Beta 1 
Tue09/18Control loops & invariants7(Scode 
Thu09/20Events & responses8(Scode Lab 1 
Fri09/21Rec: Eventful tactical proofs in KeYmaera X
Tue09/25Reactions & delays9
Thu09/27Differential equations & differential invariants10Asst 2 
Fri09/28Rec: Events to delays and flying with differential invariantsBeta 2 
Tue10/02Differential equations & proofs11
Thu10/04Ghosts & differential ghosts12Lab 2 
Fri10/05Rec: Differential invariants, differential cuts, rolling down a hill
Tue10/09Differential invariants & proof theory13 LMCS'12
Thu10/11Reviewing logical foundations & CPS LICS'12 Asst 3 
Fri10/12Rec: Proving differential equations with cuts and differential ghosts
Tue10/16Hybrid systems & games14 TOCL'15
Thu10/18MidtermBeta 3 
Fri10/19Free: Mid-semester break
Tue10/23Winning strategies & regions15 TOCL'15
Thu10/25Winning & proving hybrid games16 TOCL'15 Lab 3 
Fri10/26Free: Inauguration. Game semantics, Geri's game, and Bus gamesWhite paper 
Tue10/30Game proofs & separations17 TOCL'15 TOCL'17
Thu11/01Verified models & verified runtime validation19 FMSD'16 Asst 4 
Fri11/02Rec: Fun and games with proofsBeta 4 
Tue11/06Axioms & uniform substitutions18 JAR'17
Thu11/08Differential axioms & uniform substitutions18 JAR'17 Lab 4 
Fri11/09Rec: Uniform subst and review
Thu11/15Final examAsst 5 
Fri11/16Rec: Project modeling, baseball proving, decomposing models, logical model-predictive controlProposal 
Tue11/20Free: Project day
Thu11/22Free: Thanksgiving
Fri11/23Free: Thanksgiving
Tue11/27Virtual substitution & real equations20
Thu11/29Virtual substitution & real arithmetic21,
Fri11/30Rec: Real arithmetic for real
Tue12/04Distributed systems & hybrid systems LMCS'12
Thu12/06Model checking & reachability analysis HBMC'18 Project 
Fri12/07Rec: Prepare for Grand PrixPaper 
Tue12/11CPS 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, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | doi | book | web | abstract]

Lab Schedule

Asst 00Preparation AssignmentFri 08/31
Lab 010Scavenger HuntcodeThu 09/06
Asst 160Introduction to Hybrid ProgramsThu 09/13
Beta 120Charging Station (Betabot)codeFri 09/14
Lab 170Charging Station (Veribot)codeThu 09/20
Asst 260Loops and ProofsThu 09/27
Beta 220Follow the Leader (Betabot)codeFri 09/28
Lab 280Follow the Leader (Veribot)codeThu 10/04
Asst 360Proofs, Diamonds, Differential InvariantsThu 10/11
Beta 320Robots on Racetracks (Betabot)Thu 10/18
Lab 380Robots on Racetracks (Veribot)Thu 10/25
Asst 460Differential Invariants, Cuts, and Being GhostlyThu 11/01
Beta 420Static and Dynamic Obstacles (Betabot)Fri 11/02
Lab 480Static and Dynamic Obstacles (Veribot)Thu 11/08
Asst 560Play Around with Hybrid GamesThu 11/15
White paper20Star-lab White PaperFri 10/26
Proposal80Star-lab ProposalFri 11/16
Project100Star-lab Final ProjectThu 12/06
Paper100Term PaperFri 12/07
Slides0Slides and PresentationTue 12/11
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.