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

Textbook chapters for the individual lectures are linked below, including supporting slides marked with (S). Slides do not always cover the full lecture. The textbook this semester is brand new and significantly updated from prior lecture notes. New lecture videos were also recorded this semester and are being made available.


DateLecture NotesChExtraDue
Tue08/28Cyber-physical systems: introduction1(V) (S
Thu08/30Differential equations & domains2(V) (S
Fri08/31Rec: Syntax, Semantics, FOL, ODEsAsst 0 
Tue09/04Choice & control3(V) (S
Thu09/06Safety & contracts4(V) (SLab 0 
Fri09/07Rec: Logic, programs, transition relations
Tue09/11Dynamical systems & dynamic axioms5(V) (Scode 
Thu09/13Truth & proof6(V) (SAsst 1 
Fri09/14Rec: Common modeling errors and soundnesscode Beta 1 
Tue09/18Control loops & invariants7(V) (Scode 
Thu09/20Events & responses8(V) (Scode Lab 1 
Fri09/21Rec: Eventful tactical KeYmaera X proofscode 
Tue09/25Reactions & delays9(V) (Scode 
Thu09/27Differential equations & differential invariants10(V) (Scode Asst 2 
Fri09/28Rec: Time-triggered control and flying with differential invariantscode Beta 2 
Tue10/02Differential equations & proofs11(V) (Scode 
Thu10/04Ghosts & differential ghosts12(V) (Scode Lab 2 
Fri10/05Rec: Differential invariants, differential cutscode 
Tue10/09Differential invariants & proof theory13(V) (S
Thu10/11Hybrid systems & games14(V) (SAsst 3 
Fri10/12Rec: ODE proofs and hybrid gamesCheck 3 
Tue10/16Reviewing logical foundations & CPS
Thu10/18MidtermBeta 3 
Fri10/19Free: Mid-semester break
Tue10/23Winning strategies & regions15(V) (S
Thu10/25Winning & proving hybrid games16(V) (Scode Lab 3 
Fri10/26Free: InaugurationWhite paper 
Tue10/30Verified models & verified runtime validation19(SFMSD'16
Thu11/01Axioms & uniform substitutions18(SJAR'17Asst 4 
Fri11/02Rec: Fun and games with proofscode Beta 4 
Tue11/06Game proofs & separations17(V) (STOCL'17
Thu11/08Differential axioms & uniform substitutions18(SJAR'17Lab 4 
Fri11/09Rec: Convergence and uniform substcode 
Thu11/15Final examAsst 5 
Fri11/16Rec: KeYmaera X Tips and Trickscode Proposal 
Tue11/20Free: Project day
Thu11/22Free: Thanksgiving
Fri11/23Free: Thanksgiving
Tue11/27Virtual substitution & real equations20(V) (S
Thu11/29CPS information-flow security and smartgridsLICS'18
Fri11/30Rec: Real arithmetic for realcode 
Tue12/04Virtual substitution & real arithmetic21(V) (S) , extra
Thu12/06Distributed systems & hybrid systems(SLMCS'12Project 
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, 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 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
Check 310Robots on Racetracks (Checkbot)codeFri 10/12
Beta 320Robots on Racetracks (Betabot)codeThu 10/18
Lab 370Robots on Racetracks (Veribot)codeThu 10/25
Asst 460Differential Invariants, Cuts, and Being GhostlyThu 11/01
Beta 420Static and Dynamic Obstacles (Betabot)codeFri 11/02
Lab 480Static and Dynamic Obstacles (Veribot)codeThu 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.