[TYPES/announce] Postdoc at Imperial on the IRIS project, on "Compositional Reasoning for High-Assurance Many-Core Software"

[Alastair Donaldson]

Dear all

I'd be really grateful if you could help me spread the word about this 
postdoc position, and do contact me if you'd like to know more about it.

Best wishes

Ally Donaldson

Research Associate in Compositional Reasoning for High-Assurance 
Many-Core Software
=======================================================================

The position is for 2.5 years, with a possible extension.  Closing date 
for applications: 1 July 2018.

We are looking to hire a motivated Research Associate to join IRIS: 
Interface Reasoning for Interacting Systems - an exciting new 
EPSRC-funded Programme Grant led by University College London, Imperial 
College London, Queen Mary University of London and the London School of 
Economics. The goal of the IRIS project is to study and devise novel 
approaches for analysing large systems in a scalable manner via 
reasoning at the level of inter-component interfaces. The current post 
at Imperial College London will be jointly supervised by Dr Alastair 
Donaldson (Department of Computing) and Dr John Wickerson (Department of 
Electrical and Electronic Engineering, EEE), and will focus on reasoning 
about software designed to run on many-core architectures and other 
highly parallel accelerators. There will be a special focus on 
high-assurance software that needs to leverage many-core technology due 
to performance constraints, and yet which needs to be highly reliable.

Imperial’s Computing and EEE departments are both leading departments in 
their respective subjects among UK Universities, and have consistently 
been awarded the highest research rating from the Higher Education 
Funding Council. The 2014 REF assessment ranked the Department of 
Computing third (first in the Research Intensity table published by The 
Times Higher), and the EEE department first for research in the 
country’s EEE sector.

Reasoning about many-core software is challenging for various reasons, 
including the state-space explosion that arises due to interleaving of 
concurrent components, the subtle relaxed memory semantics of modern 
architectures and programming languages, and the difficulty of automated 
testing in the face of the nondeterminism that arises from both of these 
concerns. As part of the IRIS project we will focus on making both 
theoretical and practical advances in reasoning capabilities for 
many-core software, following various lines of inquiry including (but 
not limited to):
•    Specification-based conformance testing. For example: can a 
concurrent program’s pre- and post-conditions be used to automatically 
generate conformance tests to check that an implementation meets its 
specification?
•    Composition of memory models. For example: if a GPU, an FPGA 
accelerator and an ordinary processor all have access to the same memory 
locations, as they do on modern system-on-chip devices, what guarantees 
can programmers rely on?
•    Validation of many-core compilers. For example: can automated 
program generation techniques for testing compilers be extended and 
combined with systematic concurrency testing techniques to check that 
many-core code is compiled correctly?
•    Refinement-based parallel program construction. For example, can 
the common practice of deriving a high performance parallel program via 
a series of equivalent, increasingly optimised program variants be 
formalised and mechanised to allow automated exploration of the space of 
equivalent-by-construction implementations?
The techniques we develop will be evaluated on case studies stemming 
from the academic and industrial partners of the IRIS project, with a 
particular focus on high-performance implementations of security- and 
safety-critical functions, e.g. arising in cryptography or machine vision.

Duties and responsibilities
=====================

The successful candidate will work with the investigators at Imperial to 
conduct original research in areas relevant to the IRIS project 
(including for example some of the research areas outlined above), and 
will collaborate with the investigators and researchers involved in the 
IRIS project more broadly to amplify the technical depth and potential 
impact of the work. In addition to frequent research meetings at 
Imperial, the candidate will attend regular IRIS project meetings to 
engage with the other academic and industrial partners, and will present 
work arising from the project at international meetings.

Essential requirements
==================

The breadth of the project allows for flexibility in the profile of 
applicants, ranging from applicants with backgrounds in formal methods 
or programming languages theory who are interested in applying 
fundamental theory to challenging engineering problems, to applicants 
with a background in system-building who are interested in how to reason 
about systems. All applicants require the following:
•    a strong computing background;
•    experience either in working on state-of-the-art theoretical 
frameworks for program reasoning (such as program logics), or building 
and working with practical verification/testing tools;
•    a desire to learn about many-core systems in detail;
•    a strong research track record and publications in a relevant area 
with an ambition to lead high-quality research; and
•    excellent verbal and written communication skills.
The successful applicant will have, or be near to completing, a PhD (or 
equivalent) in an area pertinent to the subject area.

For more information:

https://www.imperial.ac.uk/jobs/description/ENG00364/research-associate-compositional-reasoning-high-assurance-many-core-software

Please get in touch with Alastair Donaldson or John Wickerson for 
informal enquiries.