Sergiy Bogomolov

Address
IST Austria
Am Campus 1
A-3400 Klosterneuburg
Austria

E-Mail
firstname.lastname@ist.ac.at


Research Interests

Trustworthy cyber-physical systems, formal methods, reliable software, model-based software development, bug finding, hybrid planning, systems biology

Research

I am currently a postdoctoral researcher in Thomas A. Henzinger's group at the Institute of Science and Technology Austria (IST Austria). I completed my PhD at the University of Freiburg, Germany in 2015 under the supervision of Andreas Podelski.


My research broadly concerns the development of algorithms for the analysis of hybrid systems. In particular, I am interested in directed model checking approaches for hybrid systems and developing precise yet efficient abstractions of them. Also, we have recently been exploring the applicability of symbolic methods to the hybrid planning domain. In addition to that, we are examining the biological models by using the notion of hybrid systems. For more details please refer to my CV.

News

Publications

  • NEW: Discrete Abstraction of Multiaffine Systems, accepted at HSB 2016, together with Hui Kong, Ezio Bartocci, Radu Grosu, Thomas A. Henzinger, Yu Jiang and Christian Schilling [pdf | bib]
  • NEW: 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 | bib]
  • NEW: High-level Hybrid Systems Analysis with Hypy, accepted at ARCH 2016, together with Stanley Bak and Christian Schilling [pdf | bib]
  • NEW: Benchmark for Verification of Fault-Tolerant Clock Synchronization Algorithms, accepted at ARCH 2016, together with Christian Herrera and Wilfried Steiner [pdf | bib]
  • NEW: Demo: Hybrid Systems Model Transformations with HyST [pdf | bib]
  • NEW: Embedding Hybrid Automata in Model-Based Design for Cyber-Physical Systems, submitted to iFM 2016, together with Stanley Bak, Omar Ali Beg, Taylor T. Johnson, Luan Viet Nguyen and Christian Schilling [pdf | bib]
  • NEW: 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 | bib ]
  • Abstraction-based Parameter Synthesis for Multiaffine Systems, HVC 2015, together with Christian Schilling, Ezio Bartocci, Gregory Batt, Hui Kong and Radu Grosu [ pdf | bib ] 
  • XSpeed: Accelerating Reachability Analysis on MultiCore Processors. HVC 2015, together with Rajarshi Ray, Amit Gurung, Binayak Das, Ezio Bartocci and Radu Grosu [ pdf | bib ]
  • 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 | bib ]
  • Runtime Verification of Model-based Development Environments. RV 2015, together with Luan Nguen, Christian Schilling, and Taylor T. Johnson [ pdf | bib ] 
  • 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 | bib] 
  • 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 | bib] 
  • HYST: A Source-to-Source Transformation Framework for Hybrid Automata, SNR 2015, together with Sergiy Bogomolov, Stanley Bak and Taylor T. Johnson. [ pdf | bib ]
  • Benchmark Generator for Stratified Controllers of Tank Networks, ARCH 2015, together with Stanley Bak, Marius Greitschus and Taylor T. Johnson [ pdf | bib ]
  • PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior, ICAPS 2015, together with  Daniele Magazzeni, Stefano Minopoli and Martin Wehrle [ pdf | bib ].
  • Eliminating Spurious Transitions in Reachability with Support Functions, HSCC 2015, together with Goran Frehse, Marius Greitschus, Thomas Strump and Andreas Podelski [ pdf | bib ]
  • HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models, HSCC2015, together with Stanley Bak and Taylor T. Johnson [ pdf | bib ]. Here you can find the supporting material.
  • 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 | bib]
  • Planning as Model Checking in Hybrid Domains, AAAI2014, together with Daniele Magazzeni, Andreas Podelski and Martin Wehrle [ pdf | bib ]. 
  • Quasi-Dependent Variables in Hybrid Automata, HSCC2014, together with Christian Herrera, Marco Muñiz, Bernd Westphal and Andreas Podelski [ pdf | bib ]. Here you can find the supporting material.
  • 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 | bib ] 
  • 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 | bib ]
  • Shape-based barrier estimation for RNAs, GCB 2010, together with Martin Mann, Björn Voß, Andreas Podelski and Rolf Backofen [ pdf | bib ]
  • Composing Reachability Analyses for Stability Analysis of Hybrid Systems, ATVA 2010, together with Corina Mitrohin and Andreas Podelski [ pdf | bib ]
  • DBLP

Thesis

Software

  • 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.

Service

Teaching

University of Freiburg:

  • Lecture Course: Software Engineering, Teaching Assistant, Summer Term 2014
  • Seminar: Design and Analysis of Cyber-Physical Systems, Winter Term 2013/14
  • Seminar: Cyber-Physical Systems - Hybrid Models, Summer Term 2013
  • Lecture Course: Hybrid Systems, Teaching Assistant, Summer Term 2013
  • Seminar: Cyber-Physical Systems, Summer Term 2011
  • Lecture Course: Model Checking, Teaching Assistant, Summer Term 2011
  • Seminar: Design and Analysis of Embedded Systems, Winter Term 2010/11
  • Lecture Course: Theoretical Computer Science II, Teaching Assistant, Winter Term 2010/11
  • Lecture Course: Informatik III - Theoretische Informatik, Teaching Assistant, Winter Term 2010/11
  • Seminar: Abstraction Techniques for Hybrid Systems, Summer Term 2010
  • Seminar: Design and Analysis of Cyber-Physical Systems, Winter Term 2009/2010
  • Lecture Course: Model Checking, Teaching Assistant, Summer Term 2009