9:30 AM – 10:00 AM

• Inauguration function

10:00 AM – 10:30 AM

• Tea Break

Lecture 1 (SM) 10:30 AM – 12:00 PM

• Motivation; Modeling Discrete Systems; Automata; HIOA specification Language; Invariants

Lecture 2 (PB) 12:00 PM – 1:30 PM

• Turing Machines, Languages and Decidability; Complexity classes, P, NP, NL, PSPACE; NL Completeness of Reachability

Tutorial 1 (SM) 3:00 PM – 5:00 PM

• An introduction to modern SMT solvers; DPLL algorithm; Examples from real-time distributed algorithms; Z3 tutorial

Lecture 3 (SM) 9:30 AM – 11:00 AM

• Computational Tree Logic (CTL) and CTL model checking

Lecture 4 (SM) 11:30 PM – 1:00 PM

• Introduction to dynamical systems and hybrid automata; Reachability; Examples and Case studies

Tutorial 2 (SM) 2:30 PM – 4:30 PM

• Reachability analysis with SpaceEx. Case studies on control systems, robotic models

Lecture 5 (SM) 9:30 AM – 11:00 AM

• Compositions, abstractions and simulation

Lecture 6 (SM) 11:30 PM – 1:00 PM

• Timed automata; Timed to rectangular hybrid automata; Undecidable problems

Tutorial 3 (PB) 2:30 PM – 4:30 PM UPPAAL HyTech.

• Model checking with UPPAAL/HyTech. Real-time systems.

Lecture 7 (SM) 9:30 AM – 11:00 AM

• Simulation-driven Verification

Lecture 8 (SM) 11:30 PM – 1:00 PM

• Stability verification, Dynamical systems, Lyapunov functions; hybrid systems, Multiple Lyapunov functions, dwell time

Tutorial 4 (SM) 2:30 PM – 4:30 PM

• C2E2 Tutorial; Case studies on autonomous vehicle maneuvers, cardiac cell models

Lecture 9 (SM) 9:30 AM – 11:00 AM

• Formal synthesis

Lecture 10 (SM) 11:30 PM – 1:00 PM

• Verification of machine learning and other hot research topics

Examination 2:30 PM – 4:30 PM

• Course Assessment Test (Optional) for participants who need a grade card for the course.