I am searching for prospective PhD students to join my interdisciplinary research group at University of Warsaw. Earliest start in September 2019.
  • Full-time contract covered by NAWA grant PPN/PPO/2018/1/00029 , monthly salary around 5800 PLN for 3,5 years + many benefits (13th salary and open possibility of applying for the basic PhD scholarship sponsored by the department and other scholarships and grants (e.g. from Polish national science fund NCN) ).
  • Interdisciplinary research on verification of cyber-physical systems controlled using neural networks + reliable AI + reinforcement learning. Full description below
  • Publications on major CS conferences including CAV, ICML, IEEE CDC, NIPS verification workshop track.
  • I encourage combining the PhD studies with internships in industry/international laboratories. I closely collaborate with worldwide renowned institutions (including UC San Diego, Stony Brook, Rutgers, TU Wien).


  • passion for research,
  • proficient in programming (C++/Python).

Please reach me with any questions, apply by sending CV to my gmail account.

Best, Jacek Cyranka

Safety verification of cyber-physical systems controlled using deep neural networks and safe AI

deep neural network controllers

Question we address: How to show that an autonomous vehicle (e.g. self-driving car) never collides with an obstacle?


Cyber-Physical systems denote various mechanizm that are controlled or monitored by computer algorithms The recent trend in CPS engineering autonomous cyber-physical systems (CPS) is to deploy a deep neural network (DNN) as a CPS controller. Some safety critical industrial applications include

  • Self driving cars developed by most of the major car makers
  • Autonomous space-ships, developed for example by NASA
  • Robotic arms developed for medical surgeries

The main concern about CPS development is the safety. Provably verifying safety properties of CPS is crucial for the engineering practice. Errors in CPS can lead to disastrous consequences, prominent examples include the Ariane 5 rocket crash in 1996. It is often crucial, especially when DNN controllers are in use, to demonstrate that for example an autonomous mobile never collides with obstacles on some given race track, or a spaceship reaches its destination and lands succesfully. Widely available computational power makes this question answerable using specialized computer algorithms.
Such algorithms are blending together modern techniques from several areas of computer science and mathematics, including interval arithmetic, numerical analysis, differential equations and machine learning.

Lagrangian reachability

In this context I have led research on a scalable algorithm for verification of safety of DNN controlled CPS based on the concept of Lagrangian Reachability [1,2]. The current research is assuming that the mathematical model of CPS is given as differential equations. Definition of arbitrary complicated CPS, its controller, parameters and initial set are parsed from an input file. To verify e.g. safety property of the provided input system, the solution set starting at the provided initial state set must be bounded. Due to the model complexity and nonlinearity the solutions are not in closed form. Hence, the algorithm (LRT) to be sound must combine numerical methods and advanced algorithms. To guarantee conservativeness all numerical computations are performed using interval arithmetic.

Currently international research team involving researchers including UC San Diego, Texas Tech and TU Wien have been working on implementing scalable LRT algorithm in C++. Current efforts are on verifying that a simple neural circuit inspired by C-Elegans worm trained using reinforcement learning [3] is able to stabilize a cart-pole, perform parallel parking, and some related control tasks. One appealing design strategy for controllers is to use deep neural networks (DNNs). Safety properties of such controllers, however, remain largely unknown. I remark that this research falls into the topic of reliable/explainable AI, which is emerging as one of the most important problems in modern engineering.

Model free control based on Reinforcement Learning

Our current algorithm, although being state of the art assumes that the model is given as differential equations. Recent effort of engineering is however focused on model-free techniques where optimal control is performed by utilizing data input only, e.g. sensor readings or video camera input. Image input can be handled by using convolutional neural networks (CNNs).

As a future research, we will work on extending our techniques to the settings, where the exact model is not given / not known at all. It will require however establishing reliable reinforcement methods, e.g. policy gradient and safe AI in general. We will be utilizing major machine learning packages, and implement in Python.


[1] Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul Jones, Scott A. Smolka, Radu Grosu, Lagrangian Reachability, CAV 2017
[2] Jacek Cyranka, Md. Ariful Islam, Scott A. Smolka, Sicun Gao, Radu Grosu, Tight Continuous-Time Reachtubes for Lagrangian Reachability, IEEE CDC 2018
[3] Mathias Lechner, Radu Grosu, Ramin M. Hasani, Worm-level Control through Search-based Reinforcement Learning, NIPS 2017

Target conferences:

  • CAV
  • ICML
  • NeurIPS (verification workshop track)

Collaborators include:

  • Radu Grosu (TU Wien)
  • Arif Islam (Texas Tech)
  • Scott Smolka (Stony Brook)
  • Sicun Gao (UCSD)