General

OBJECTIVE
The objective of the course is to expand upon basic notions of verification and develop a thorough understanding of probabilistic model checking over Markov models. Lectures will cover algorithms for verification and synthesis. Towards the end of the course, we provide an introduction to advanced topics and vistas in probabilistic models and in verification techniques and tools.

INSTRUCTOR
Alessandro Abate is Professor of Verification and Control at the Computer Science Department of the University of Oxford (https://www.cs.ox.ac.uk/people/alessandro.abate/), where he also served as Deputy Head of Department. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received a Laurea degree from the University of Padua and MS/PhD at UC Berkeley. His research work spans logic, probability, control, and AI. His interests lie in the analysis, verification, and optimal control of heterogeneous and complex dynamical models and in their applications in cyber-physical systems, particularly in assured autonomy and energy systems.