Sergiy Bogomolov

Sergiy is a Reader / Associate Professor in Cyber-Physical Systems at Newcastle University (UK). Sergiy joined Newcastle University from Australian National University (Australia) in September 2019. Prior to being a faculty member at ANU, Sergiy was a postdoctoral researcher at the Institute of Science and Technology Austria (IST Austria). His research focuses on the development of algorithms and tools to model and analyze complex concurrent and distributed systems. In particular, Sergiy aims at providing scalable solutions for automatic analysis of cyber-physical systems using the techniques on the interface of the areas of verification, control and artificial intelligence. Sergiy has over 40 publications in top hybrid systems, verification and AI venues, such as EMSOFT, HSCC, TACAS, AAAI, IJCAI and ICAPS targeting multiple applications domains such as autonomous systems, systems biology and operations research. He has co-chaired several events (FORMATS'22, HSCC'21, SNR'15-17, NSV'15-16, MOCHAP'15), served on the program committees of around 50 conferences and workshops; he was also ACM SIGBED Review Editor in 2017-2019. Sergiy's work has won several awards such as Best Repeatability Evaluation Package Award at HSCC'16, Best Tool Award at ARCH'16 and Best Paper Award at HVC'14. He started the International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT in 2015 (collocated with CAV, Cyber-Physical Systems Week and ETAPS in different years). In order to ensure his research has a lasting impact in the community, Sergiy actively pursues research collaborations and has been supported by a number of agencies and companies. These include US Air Force Office of Scientific Research, Defence Science and Technology Group (Australia) and Toyota (USA). His Ph.D. and M.Sc. degrees are from the University of Freiburg (Germany).

For more information, please check out Sergiy's CV, as well as his DBLP and Google Scholar entries.

Cyber-physical systems and artificial intelligence.

• Paulius Stankaitis, postdoctoral researcher, since April 2020
• Kostiantyn Potomkin, PhD student, since November 2017
• Abdelrahman Hekal, PhD student, since September 2020

I always look for excellent  PhD students interested in developing novel methods to design and analyze cyber-physical systems (e.g., autonomous cars). The main focus will be on the formal verification of hybrid systems, i.e., dynamical systems exhibiting mixed discrete-continuous behaviour. Depending on the interest and background of candidates, research can include topics from AI as well, e.g., AI planning and machine learning.  

Candidate profile:

• strong background in Computer Science and/or Mathematics  (particularly numerical methods, differential equations, control and optimisation theory) 
• solid programming skills in C++/Java/Python/Matlab 
• should have completed, or about to complete, a Bachelor's or Master's degree in Computer Science or related areas

Please send me a complete CV as well as your transcripts. 

• Reachability analysis of linear hybrid systems via block decomposition, EMSOFT 2020, together with Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling [ pdf ]
• Safety verification for random ordinary differential equation, EMSOFT 2020, together with Bai Xue, Martin Fränzle, Naijun Zhan and Bican Xia [ pdf ]
• Reachability analysis of nonlinear systems using hybridization and dynamics scaling, FORMATS 2020, together with Dongxu Li and  Stanley Bak [ pdf ]
• Safety verification for impulsive systems,  IFAC World Congress, 2020, together with Petro Feketa and Thomas Meurer [ pdf published at the conference; pdf with errata ]
• Falsification of hybrid systems using symbolic reachability and trajectory splicing, HSCC 2019, together with Goran Frehse, Amit Gurung, Dongxu Li, Georg Martius, and Rajarshi Ray [ pdf ] 
• JuliaReach: a toolbox for set-based reachability, HSCC 2019, together with Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling [ pdf ] 
• Temporal planning as refinement-based model checking, ICAPS 2019, together with Alexander Heinz, Martin Wehrle, Daniele Magazzeni, Marius Greitschus, and Andreas Podelski [ pdf ]
• Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices, HSCC 2018, together with Marcelo Forets, Goran Frehse, Andreas Podelski, Christian Schilling, and Frédéric Viry [ pdf ] 
• Effect-abstraction based relaxation for linear numeric planning, IJCAI 2018, together with Dongxu Li, Enrico Scala and Patrik Haslum [ pdf ] 
• Parallel reachability analysis of hybrid systems in XSpeed, STTT 2018, together with Amit Gurung, Rajarshi Ray, Ezio Bartocci and Radu Grosu [ pdf ] 
• Time-triggered conversion of guards for reachability analysis of hybrid automata, FORMATS 2017, together with Stanley Bak and Matthias Althoff [ pdf ]
• Conic abstractions for hybrid systems, FORMATS 2017, together with Mirco Giacobbe, Thomas A. Henzinger and Hui Kong [ pdf ]
• Hybrid automata: from verification to implementation, STTT 2017, together with Stanley Bak, Omar Ali Beg, Taylor T. Johnson, Luan Viet Nguyen, and Christian Schilling [ pdf ]
• Challenges and tool implementation of hybrid rapidly-exploring random trees, NSV 2017, together with Stanley Bak, Thomas A. Henzinger, and Aviral Kumar [ pdf ]
• Counterexample-guided refinement of template polyhedra, TACAS 2017, together with Goran Frehse, Mirco Giacobbe, and Thomas A. Henzinger [ pdf ]
• Safety verification of nonlinear hybrid systems based on invariant clusters, HSCC 2017, together with Hui Kong, Christian Schilling, Yu Jiang, and Thomas Henzinger [ pdf ]
• Discrete Abstraction of Multiaffine Systems, HSB 2016, together with Hui Kong, Ezio Bartocci, Radu Grosu, Thomas A. Henzinger, Yu Jiang and Christian Schilling [ pdf ]
• Adaptive moment closure for parameter inference of biochemical reaction networks, Biosystems 2016, together with Christian Schilling, Thomas A. Henzinger, Andreas Podelski and Jakob Ruess and  [ pdf ]
• High-level Hybrid Systems Analysis with Hypy, ARCH 2016, together with Stanley Bak and Christian Schilling [ pdf ]
• Benchmark for Verification of Fault-Tolerant Clock Synchronization Algorithms, ARCH 2016, together with Christian Herrera and Wilfried Steiner [ pdf ]
• Demo: Hybrid Systems Model Transformations with HyST, HSCC 2016, together with Stanley Bak and Taylor T. Johnson [ pdf ]
• Scalable Static Hybridization Methods for Analysis of Nonlinear Systems, HSCC 2016, together with Stanley Bak,Thomas A. Henzinger, Taylor T. Johnson and Pradyot Prakash [ pdf ]
• Abstraction-based Parameter Synthesis for Multiaffine Systems, HVC 2015, together with Christian Schilling, Ezio Bartocci, Gregory Batt, Hui Kong and Radu Grosu [ pdf ] 
• XSpeed: Accelerating Reachability Analysis on MultiCore Processors. HVC 2015, together with Rajarshi Ray, Amit Gurung, Binayak Das, Ezio Bartocci and Radu Grosu [ pdf ]
• Adaptive moment closure for parameter inference of biochemical reaction networks. CMSB 2015, together with Thomas A. Henzinger, Andreas Podelski, Jakob Ruess and Christian Schilling [ pdf ]
• Runtime Verification of Model-based Development Environments. RV 2015, together with Luan Nguen, Christian Schilling, and Taylor T. Johnson [ pdf ] 
• Co-Simulation of Hybrid Systems with SpaceEx and Uppaal, MODELICA 2015, together with Marius Greitschus, Peter G. Jensen, Kim G. Larsen, Marius Mikučionis, Thomas Strump and Stavros Tripakis [pdf ] 
• Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions, invited journal article at STTT2015 together with Alexandre Donze, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle. Here you can find the paper and supporting material. [ pdf ] 
• Benchmark Generator for Stratified Controllers of Tank Networks, ARCH 2015, together with Stanley Bak, Marius Greitschus and Taylor T. Johnson [ pdf ]
• PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior, ICAPS 2015, together with  Daniele Magazzeni, Stefano Minopoli and Martin Wehrle [ pdf ]
• Eliminating Spurious Transitions in Reachability with Support Functions, HSCC 2015, together with Goran Frehse, Marius Greitschus, Thomas Strump and Andreas Podelski [ pdf ]
• HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models, HSCC2015, together with Stanley Bak and Taylor T. Johnson [ pdf ]
• Assume-Guarantee Abstraction Refinement Meets Hybrid Systems, HVC 2014, together with Goran Frehse, Marius Greitschus, Radu Grosu, Corina Pasareanu, Andreas Podelski, and Thomas Strump. Best Paper Award. [ pdf ]
• Planning as Model Checking in Hybrid Domains, AAAI2014, together with Daniele Magazzeni, Andreas Podelski and Martin Wehrle [ pdf ] 
• Quasi-Dependent Variables in Hybrid Automata, HSCC2014, together with Christian Herrera, Marco Muñiz, Bernd Westphal and Andreas Podelski [ pdf ]
• Abstraction-Based Guided Search for Hybrid Systems, SPIN2013, together with Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle [ pdf ] 
• A Box-based Distance between Regions for Guiding the Reachability Analysis of SpaceEx, CAV2012, together with  Radu Grosu, Goran Frehse, Hamed Ladan, Andreas Podelski and Martin Wehrle [ pdf ]
• Shape-based barrier estimation for RNAs, GCB 2010, together with Martin Mann, Björn Voß, Andreas Podelski and Rolf Backofen [ pdf ]
• Composing Reachability Analyses for Stability Analysis of Hybrid Systems, ATVA 2010, together with Corina Mitrohin and Andreas Podelski [ pdf ]

• Abstraction-based Analysis of Hybrid Automata, PhD thesis, University of Freiburg, Germany, 2015
  

• SpaceEx with guided state space exploration, a version of hybrid model checker SpaceEx adjusted towards solving falsification problems, i.e., our primary goal is to find a path to the bad states as fast as possible. To do that we have introduced two heuristics which prioritize symbolic successors during the exploration of the state space of a considered hybrid system: box-based heuristic and PDB heuristic. The following presentation describes both the approaches.
• SpaceEx with assume guarantee abstraction refinement  allows for the compositional analysis of large systems consisting of multiple components. In order to build assumptions we introduce an appropriate abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement.