Formal Verification of Safety-Critical Systems

Margarita Korovina

(A.P. Ershov Institute of Informatics Systems, Novosibirsk)

In this talk we present ongoing research which is aimed at creating a logical framework for formal verification of definable dynamical systems. We address reachability problem, i.e., whether trajectories of the dynamical systems reach safe/unsafe regions from initial regions. The key idea of our approach is based on computing combinatorial types of trajectories. We show how it could be done using cylindrical cell decomposition for polynomial and Pfaffian dynamics.

Tuesday 19th January 2016, 14:00
Robert Recorde Room
Department of Computer Science