[TYPES/announce] Multiple postdoc and PhD positions on verification, concurrency and model learning at University College London and Royal Holloway University of London (Deadline Jan 5, 2020)

[Matteo Sammartino]

We invite applications for:

  - *two* Research Fellow/Senior Research Fellow positions (Deadline: January 5, 2020). Positions are 1 year in the first instance, with the possibility of extension until December 2022. One position will be at University College London, and one at Royal Holloway University of London.

  - *one* PhD studentship at UCL.

Successful applicants will be working on the EPSRC-funded "Verification of Hardware Concurrency via Model Learning" (CLeVer) project.

This is a joint research endeavour involving the Computer Science Departments of two UK's leading research-intensive universities -- University College London and Royal Holloway University of London -- and ARM, world-leading designer of multi-core chips.

We are looking for candidates with experience in one or more of the following areas: model learning techniques, verification, concurrency, and formal methods. Experience in tool implementation will also be valued.


# HOW TO APPLY


- Applications for *both* the (Senior) Research Fellow positions should be made here before *January 5, 2020*:

https://atsv7.wcn.co.uk/search_engine/jobs.cgi?owner=5041404&ownertype=fair&jcode=1847641&vt_template=965&adminview=1


- Applications for the PhD position should be made here:

https://www.ucl.ac.uk/prospective-students/graduate/apply



Interested applicants are encouraged to contact Prof. Alexandra Silva (alexandra.silva at ucl.ac.uk) and Dr. Matteo Sammartino (m.sammartino at ucl.ac.uk).


# ABOUT THE PROJECT

Digital devices increasingly rely on multi-threaded computation, with sophisticated concurrent behaviour becoming prevalent at any scale.
As the complexity of these systems increases, there is a pressing need to automate the assessment of their correctness, especially with respect to concurrency-related aspects.

Formal verification provides highly effective techniques to assess the correctness of systems.
However, formal models are usually built by humans, and as such can be error-prone and inaccurate. 

This project aims to:

- develop a verification framework that relies on learning techniques to automatically build and verify models of concurrency, with a particular focus on multi-core systems.

- apply the framework to industrial verification tasks, in collaboration with ARM.


The project will provide opportunities for both theoretical and applied research in several areas of Computer Science, including model learning techniques, verification, concurrency, and formal methods.