PhD in Computer Science

PhD Course on “Numerical verification of nonlinear hybrid automata”

14-28 september 2020

Academic staff
Luca Geretti

Series to which this belongs

33° ciclo
34° ciclo
35° ciclo


The course offers an overview of the verification problem for nonlinear hybrid systems, in particular when modeled by hybrid automata. Compared to systems with restricted dynamics (e.g., linear systems or systems with clocks), nonlinearity limits the range of approaches available for analysis, in particular with respect to symbolic reasoning. We explore the challenges to design a numerically validated approach to verification, we introduce the state-of-art tools and finally we focus on the Ariadne library, developed in our Department in collaboration with an international team. During the lectures, there will be live demonstrations of Ariadne, and case studies for home experiments will be made available.


    Introduction to numerical verification; the problem of reachability; computable analysis
    Hybrid automata and the different classes of expressivity
    Representations for reachable sets
    Tools for numerical verification of hybrid automata
    Computing the continuous evolution of a nonlinear system
    Computing the hybrid evolution of a nonlinear system
    Verification of nonlinear hybrid automata
    Compositionality and contract-based design


  • pdf   Flyer   (pdf, it, 100 KB, 20/07/20)