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

Textbook chapters for the individual lectures are linked below, including supporting slides marked with (⊞). 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

Date		Lecture Notes	Ch	Extra	Due
Tue	08/28	Cyber-physical systems: introduction	1	(▶) (⊞)
Thu	08/30	Differential equations & domains	2	(▶) (⊞)
Fri	08/31	Rec: Syntax, Semantics, FOL, ODEs			Asst 0
Tue	09/04	Choice & control	3	(▶) (⊞)
Thu	09/06	Safety & contracts	4	(▶) (⊞)	Lab 0
Fri	09/07	Rec: Logic, programs, transition relations
Tue	09/11	Dynamical systems & dynamic axioms	5	(▶) (⊞) code
Thu	09/13	Truth & proof	6	(▶) (⊞)	Asst 1
Fri	09/14	Rec: Common modeling errors and soundness		code	Beta 1
Tue	09/18	Control loops & invariants	7	(▶) (⊞) code
Thu	09/20	Events & responses	8	(▶) (⊞) code	Lab 1
Fri	09/21	Rec: Eventful tactical KeYmaera X proofs		code
Tue	09/25	Reactions & delays	9	(▶) (⊞) code
Thu	09/27	Differential equations & differential invariants	10	(▶) (⊞) code	Asst 2
Fri	09/28	Rec: Time-triggered control and flying with differential invariants		code	Beta 2
Tue	10/02	Differential equations & proofs	11	(▶) (⊞) code
Thu	10/04	Ghosts & differential ghosts	12	(▶) (⊞) code	Lab 2
Fri	10/05	Rec: Differential invariants, differential cuts		code
Tue	10/09	Differential invariants & proof theory	13	(▶) (⊞)
Thu	10/11	Hybrid systems & games	14	(▶) (⊞)	Asst 3
Fri	10/12	Rec: ODE proofs and hybrid games			Check 3
Tue	10/16	Reviewing logical foundations & CPS
Thu	10/18	Midterm			Beta 3
Fri	10/19	Free: Mid-semester break
Tue	10/23	Winning strategies & regions	15	(▶) (⊞)
Thu	10/25	Winning & proving hybrid games	16	(▶) (⊞) code	Lab 3
Fri	10/26	Free: Inauguration			White paper
Tue	10/30	Verified models & verified runtime validation	19	(⊞) FMSD'16
Thu	11/01	Axioms & uniform substitutions	18	(⊞) JAR'17	Asst 4
Fri	11/02	Rec: Fun and games with proofs		code	Beta 4
Tue	11/06	Game proofs & separations	17	(▶) (⊞) TOCL'17
Thu	11/08	Differential axioms & uniform substitutions	18	(⊞) JAR'17	Lab 4
Fri	11/09	Rec: Convergence and uniform subst		code
Tue	11/13	Review
Thu	11/15	Final exam			Asst 5
Fri	11/16	Rec: KeYmaera X Tips and Tricks		code	Proposal
Tue	11/20	Free: Project day
Thu	11/22	Free: Thanksgiving
Fri	11/23	Free: Thanksgiving
Tue	11/27	Virtual substitution & real equations	20	(▶) (⊞)
Thu	11/29	CPS information-flow security and smartgrids		LICS'18
Fri	11/30	Rec: Real arithmetic for real		code
Tue	12/04	Virtual substitution & real arithmetic	21	(▶) (⊞) , extra
Thu	12/06	Distributed systems & hybrid systems		(⊞) LMCS'12	Project
Fri	12/07	Rec: Prepare for Grand Prix			Paper
Tue	12/11	CPS V&V Grand Prix			Slides

The lecture schedule is tentative!

The chapter numbers indicated above refer to the following textbook:

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

Lab Schedule

	Points	Assignment		Due
Asst 0	0	Preparation Assignment		Fri	08/31
Lab 0	10	Scavenger Hunt	code	Thu	09/06
Asst 1	60	Introduction to Hybrid Programs		Thu	09/13
Beta 1	20	Charging Station (Betabot)	code	Fri	09/14
Lab 1	70	Charging Station (Veribot)	code	Thu	09/20
Asst 2	60	Loops and Proofs		Thu	09/27
Beta 2	20	Follow the Leader (Betabot)	code	Fri	09/28
Lab 2	80	Follow the Leader (Veribot)	code	Thu	10/04
Asst 3	60	Proofs, Diamonds, Differential Invariants		Thu	10/11
Check 3	10	Robots on Racetracks (Checkbot)	code	Fri	10/12
Beta 3	20	Robots on Racetracks (Betabot)	code	Thu	10/18
Lab 3	70	Robots on Racetracks (Veribot)	code	Thu	10/25
Asst 4	60	Differential Invariants, Cuts, and Being Ghostly		Thu	11/01
Beta 4	20	Static and Dynamic Obstacles (Betabot)	code	Fri	11/02
Lab 4	80	Static and Dynamic Obstacles (Veribot)	code	Thu	11/08
Asst 5	60	Play Around with Hybrid Games		Thu	11/15
White paper	20	Star-lab White Paper		Fri	10/26
Proposal	80	Star-lab Proposal		Fri	11/16
Project	100	Star-lab Final Project		Thu	12/06
Paper	100	Term Paper		Fri	12/07
Slides	0	Slides and Presentation		Tue	12/11
Sum	1000	points 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.