The University of Southampton

Dr Andrew Sogokon 

CPS PG representative


Research interests

My research interests are primarily in formal modelling and verification of hybrid systems (part of a broader family of cyber-physical systems). Most of my work to date has concerned systems whose continuous motion is governed by non-linear ordinary differential equations (ODEs).

Keywords: Formal verification, differential equations, algebra, hybrid dynamical systems.


Algorithms, mathematics for computer science, verification.


Sogokon, Andrew, Mitsch, Stefan, Tan, Yong Kiam, Cordwell, Katherine and Platzer, André (2019) Pegasus: a framework for sound continuous invariant generation. M., ter Beek, A., McIver and J., Oliveira (eds.) In Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Portugal, October 7–11, 2019, Proceedings. vol. 11800, Springer. pp. 138-157 . (doi:10.1007/978-3-030-30942-8_10).

Sogokon, Andrew and Jackson, Paul (2015) Direct formal verification of liveness properties in continuous and hybrid dynamical systems. Bjørner, Nikolaj and de Boer, Frank (eds.) In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway. Proceedings. vol. 9109, Springer. pp. 514-531 .

Sogokon, Andrew, Ghorbal, Khalil, Jackson, Paul and Platzer, André (2016) A method for invariant generation for polynomial continuous systems. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference (VMCAI 2016). Proceedings. Springer..

Sogokon, Andrew, Ghorbal, Khalil and Johnson, Taylor (2017) Operational models of piecewise-smooth systems. ACM Transactions on Embedded Computing Systems, 16 (5), 1-19, [185]. (doi:10.1145/3126506).

Sogokon, Andrew, Ghorbal, Khalil, Tan, Yong Kiam and Platzer, André (2018) Vector barrier certificates and comparison systems. In Proceedings of the 22nd International Symposium on Formal Methods, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018. Springer. pp. 1-19 .

Sogokon, Andrew, Jackson, Paul B. and Johnson, Taylor T. (2019) Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants. Journal of Automated Reasoning, 63 (4), 1005-1029. (doi:10.1007/s10817-018-9497-x).


Share this profile FacebookTwitterWeibo