Andrew Sogokon
Research Postgraduate Student at the University of Edinburgh, United Kingdom
Positive Invariance In Safety Verification
Abstract:
We explore
practical inference rules for safety verification of continuous
dynamical systems inspired by existing work in control. Sub-level sets
of differentiable functions are very convenient for defining sets in
continuous state space, however safety specifications often cannot be
cast in this form without being conservative. It is far more natural to
express system properties as Boolean formulas in which sub-level sets
are atoms. A deductive verification system would benefit greatly from
having the facility to both specify and reason effectively about
invariance of such formulas. We discuss currently existing approaches
(e.g. in KeYmaera) and possible alternative directions in furthering
this goal.
Bio: Andrew Sogokon is currently pursuing a PhD.
at the Laboratory for Foundations of Computer Science at the University
of Edinburgh, UK. His interests lie primarily in nonlinear dynamical
systems, control theory, formal verification and commutative algebra