Principles of Programming (POP) Seminar

Research Postgraduate Student
Laboratory for Foundations of Computer Science
University of Edinburgh, United Kingdom
Positive Invariance In Safety Verification
Monday, November 25, 2013 - 1:00pm to 2:00pm
Traffic21 Classroom 6501 
Gates&Hillman Centers

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

For More Information, Please Contact: