[ 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.
# 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.si...@ucl.ac.uk) and Dr. Matteo Sammartino (m.sammart...@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.
