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.
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.
Faculty Host: André Platzer
dcm [atsymbol] cs.cmu.edu