ERC funded Ph.D. positions on Formal Verification at the University of Leicester

by Nir Piterman, April 3, 2018

This PhD project is to work on techniques for automatic production of systems from high-level specifications of their behaviours. Specifically, the project concentrates on the theoretical foundations and considers topics such as two-player games and their solutions, modelling solutions for interacting agents, and temporal and strategy logic.

This is part of an European Research Council Consolidator grant awarded to Dr Nir Piterman.

Applications are invited for PhD studentships within the prestigious European Research Council (ERC) consolidator funded project “dSynMA: Distributed Synthesis from Single to Multiple Agents”. The topic of the grant is to develop techniques that enable development of autonomous collaboration between devices. For isolated (and co-existing) devices, reactive synthesis – automatic production of plans from high-level specification – is emerging as a viable tool for the development of robots and reactive software. This is especially important in the context of safety-critical systems, where assurances are required and systems need to have guarantees on performance. The project will develop theoretical frameworks that support real collaboration between devices. We will consider novel interaction and communication concepts that would create a framework of correct-by construction application of collaborating devices.

Specifically, the project includes studying two-player games and their solutions, modelling solutions for interacting agents, studying of temporal logic, and implementing tools that will show applicability of our techniques. The research will focus on the following objectives:

  1. Consider modelling frameworks that combine message passing and variable sharing allowing for synchronization as well as passage of information.
  2. Work on algorithmic analysis of games arising from combinations of multiple agents. 
  3. Study specification languages that extend temporal and strategy logic. 
  4. Implement tools that will show how these techniques can be applied in practice. 

The project team includes Dr Nir Piterman (PI), two Research Assistants (PostDocs), two other PhD students, and later on another RA. 

Informal enquiries are welcome and should be made to Dr Nir Piterman ( 

Funding details: This is a 4-year PhD studentship covering: the tuition fees (including for international students) and a tax-free stipend at RCUK rates (currently £14,553 for 2017/2018).

Further details and application.