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

  1. Home
  2. >>
  3. Courses
  4. >>
  5. FCPS Sp17
  6. >>
  7. Schedule
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.

Schedule

DateLecture NotesExtraDue
Tue01/17Cyber-physical systems: introduction(V) (S
Thu01/19Differential equations & domains(V) (S
Fri01/20Rec: ODE, FOL, prepAsst 0 
Tue01/24Choice & control(V) (S
Thu01/26Safety & contracts(V) (SLab 0 
Fri01/27Rec: Programs, properties, transitions, and examplescode 
Tue01/31Dynamical systems & dynamic axioms(V) (Scode LICS'12
Thu02/02Truth & proof(V) (SAsst 1 
Fri02/03Rec: What is a proof and why?code Beta 1 
Tue02/07Control loops & invariants(V) (Scode 
Thu02/09Events & responses(V) (Scode Lab 1 
Fri02/10Rec: Eventful tactical proofs in KeYmaera Xcode 
Tue02/14Reactions & delays(V) (Scode 
Thu02/16Differential equations & differential invariants(V) (Scode Asst 2 
Fri02/17Rec: Events to delays and flying with differential invariantscode Beta 2 
Tue02/21Differential equations & proofs(V) (Scode 
Thu02/23Ghosts & differential ghosts(V) (Scode LMCS'12, extraLab 2 
Fri02/24Rec: Differential invariants, differential cuts, rolling down a hillcode 
Tue02/28Reviewing logical foundations & CPS(V) (SLICS'12Asst 3 
Thu03/02Midterm
Fri03/03Rec: Proving differential equations with cuts and differential ghostscode Beta 3 
Tue03/07Differential invariants & proof theory(V) (SLMCS'12
Thu03/09Verified models & verified runtime validation(V) (SFMSD'16Lab 3 
Fri03/10Free: Mid-semester break
Tue03/14Free: Spring break
Thu03/16Free: Spring break
Fri03/17Free: Spring break
Tue03/21Hybrid systems & games(V) (STOCL'15
Thu03/23Winning strategies & regions(V) (STOCL'15Asst 4 
Fri03/24Rec: Game semantics, Geri's game, and Bus gamescode Beta 4 
Tue03/28Winning & proving hybrid games(V) (Scode TOCL'15
Thu03/30Game proofs & separations(V) (STOCL'15 TOCL'17Lab 4 
Fri03/31Rec: Fun and games with proofscode White paper 
Tue04/04Axioms & uniform substitutions(V) (SJAR'17
Thu04/06Differential axioms & uniform substitutions(V) (SJAR'17Asst 5 
Fri04/07Rec: Uniform subst and review
Tue04/11Recap
Thu04/13Final exam
Fri04/14Rec: Project modeling, baseball proving, decomposing models, logical model-predictive controlcode 
Tue04/18Optional: Safety & CPS ImplementationsProposal 
Thu04/20Free: Spring Carnival
Fri04/21Free: Spring Carnival
Tue04/25Virtual substitution & real equations(V) (S
Thu04/27Virtual substitution & real arithmetic(V) (S) , extra
Fri04/28Rec: Real arithmetic for realcode 
Tue05/02Distributed systems & hybrid systems(V) (SLMCS'12
Thu05/04Hybrid systems & complete proofs(SLICS'12Project 
Fri05/05Rec: Prepare for Grand PrixPaper 
Thu05/11CPS V&V Grand PrixSlides 
The lecture schedule is tentative!

Lab Schedule

PointsAssignmentDue
Asst 00Preparation AssignmentFri01/20
Lab 010Scavenger HuntcodeThu01/26
Asst 160Introduction to Hybrid ProgramsThu02/02
Beta 120Charging Station (Betabot)codeFri02/03
Lab 170Charging Station (Veribot)codeThu02/09
Asst 260Loops and ProofsThu02/16
Beta 220Follow the Leader (Betabot)codeFri02/17
Lab 280Follow the Leader (Veribot)codeThu02/23
Asst 360Proofs, Diamonds, Differential InvariantsTue02/28
Beta 320Robots on Racetracks (Betabot)codeFri03/03
Lab 380Robots on Racetracks (Veribot)codeThu03/09
Asst 460Differential Invariants, Cuts, and Being GhostlyThu03/23
Beta 420Static and Dynamic Obstacles (Betabot)codeFri03/24
Lab 480Static and Dynamic Obstacles (Veribot)codeThu03/30
Asst 560Play Around with Hybrid GamesThu04/06
White paper20Star-lab White PaperFri03/31
Proposal80Star-lab ProposalTue04/18
Project100Star-lab Final ProjectThu05/04
Paper100Term PaperFri05/05
Slides0Slides and PresentationThu05/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.