[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

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.


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


- Applications for the PhD position should be made here:


Interested applicants are encouraged to contact Prof. Alexandra Silva 
(alexandra.si...@ucl.ac.uk) and Dr. Matteo Sammartino (m.sammart...@ucl.ac.uk).


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 

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.

Reply via email to