15-819/18-879L: Hybrid Systems Analysis and Theorem Proving

15-819L: Hybrid Systems Analysis and Theorem Proving (Spring 2009)
18-879L: Hybrid Systems Analysis and Theorem Proving (Spring 2009)

Instructor:	André Platzer
Units:	12
Semester:	Spring 2009
Time:	Tue, Thu 3:00-4:20
Place:	Wean Hall 4615A
	This course is cross-listed in Computer Science as 15-819L and in Electrical & Computer Engineering as 18-879L at Carnegie Mellon University

Schedule

Date	Lecture	Assignment	Reading
Tue 01/13	Safety-critical Hybrid Systems	none	hybrid automata, examples
Thu 01/15	Differential Equations, Propositional & First-Order Logic
Tue 01/20	Interpreted First-Order Logic and the Reals
Thu 01/22	Numerical Analysis versus Symbolic Verification		handout
Tue 01/27	Propositional Tableaux and Herbrand's Theorem
Thu 01/30	First-Order Free-Variable and Ground Tableaux
Tue 02/03	Sequent Calculi
Thu 02/05	Hybrid Programs & Compositionality		handout
Tue 02/10	Hybrid Programs versus Hybrid Automata
Thu 02/12	Differential Dynamic Logic & Compositional Verification	assignment 1 due
Tue 02/17	Real Free Variables and Deduction Modulo
Thu 02/19	Soundness
Tue 02/24	Train Control Verification
Thu 02/26	Recap	assignment 2 due
Tue 03/03	Midterm Exam Slot
Thu 03/05	Midterm Exam Slot	project whitepaper due
Tue 03/10	Spring Break
Thu 03/12	Spring Break
Tue 03/17	KeYmaera & Tableau Procedures
Thu 03/19	Completeness
Tue 03/24	Differential-algebraic Programs & Disturbance in the Dynamics
Thu 03/26	Semantics of Differential-algebraic Programs & Disturbance
Tue 03/31	Aircraft, Differential-algebraic Logic & Derivations		handout
Thu 04/02	Proving Differential-algebraic Equations, Disturbance & Differential Induction
Tue 04/07	Differential Saturation, Closure Properties
Thu 04/09	Differential Variants, Transformations & Reduction	assignment 3 due	example
Tue 04/14	Differential Soundness
Thu 04/16	Spring Carnival
Tue 04/21	Deductive Power of Differential Induction
Thu 04/23	Real Gödel & Hybrid Program Renditions
Tue 04/28	Hybrid Completeness Proof
Thu 04/30	Wrap up and Outlook	Final Project Report due