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)

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: Janua=
ry 5, 2020). Positions are 1 year in the first instance, with the possibili=
ty of extension until December 2022. One position will be at University Col=
lege 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 Departmen=
ts of two UK's leading research-intensive universities -- University Colleg=
e 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 followi=
ng 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=3D5041404&ownertype=3D=
fair&jcode=3D1847641&vt_template=3D965&adminview=3D1


- 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 (alex=
andra.silva@ucl.ac.uk) and Dr. Matteo Sammartino (m.sammartino@ucl.ac.uk).


# ABOUT THE PROJECT

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

Formal verification provides highly effective techniques to assess the corr=
ectness of systems.
However, formal models are usually built by humans, and as such can be erro=
r-prone and inaccurate.=20

This project aims to:

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

- apply the framework to industrial verification tasks, in collaboration wi=
th ARM.


The project will provide opportunities for both theoretical and applied res=
earch in several areas of Computer Science, including model learning techni=
ques, verification, concurrency, and formal methods.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]