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
Hybrid Systems Analysis & Design


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