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.

Schedule

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 
Tue11/13Review
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

PointsAssignmentDue
Asst 00Preparation AssignmentFri08/31
Lab 010Scavenger HuntcodeThu09/06
Asst 160Introduction to Hybrid ProgramsThu09/13
Beta 120Charging Station (Betabot)codeFri09/14
Lab 170Charging Station (Veribot)codeThu09/20
Asst 260Loops and ProofsThu09/27
Beta 220Follow the Leader (Betabot)codeFri09/28
Lab 280Follow the Leader (Veribot)codeThu10/04
Asst 360Proofs, Diamonds, Differential InvariantsThu10/11
Check 310Robots on Racetracks (Checkbot)codeFri10/12
Beta 320Robots on Racetracks (Betabot)codeThu10/18
Lab 370Robots on Racetracks (Veribot)codeThu10/25
Asst 460Differential Invariants, Cuts, and Being GhostlyThu11/01
Beta 420Static and Dynamic Obstacles (Betabot)codeFri11/02
Lab 480Static and Dynamic Obstacles (Veribot)codeThu11/08
Asst 560Play Around with Hybrid GamesThu11/15
White paper20Star-lab White PaperFri10/26
Proposal80Star-lab ProposalFri11/16
Project100Star-lab Final ProjectThu12/06
Paper100Term PaperFri12/07
Slides0Slides and PresentationTue12/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.