[TYPES/announce] Postdoctoral position, concurrency reasoning, Imperial College London

[Gardner, Philippa A]

Hello all,

We are looking to recruit one postdoctoral researcher in the Program
Specification and Verification Group at Imperial College London, to work
on reasoning about concurrent programs. The position is suitable for
either a theoretician, who would work on the foundations of concurrent
reasoning, or a theoretician/practitioner, who would work on the
verification and testing of file systems. If interested, please send
your CV and Research Summary to me by September 18th.

This position will have an initial duration of 2.5 years, with a certain
level of flexibility with respect to the start date and possible
extensions. It will be funded as part of the £5.6M EPSRC Programme Grant
“REMS: Rigorous Engineering of Mainstream Systems”, at the University of
Cambridge, University of Edinburgh, and Imperial College London (see
http://www.cl.cam.ac.uk/~pes20/rems/).

The Department of Computing at Imperial provides a vibrant and
stimulating research environment in the heart of London, with leading
research groups working on programming languages, verification, and
testing. The quality of the Department has been consistently awarded the
highest research and teaching rating. In the latest Research Excellence
Framework assessment of 2014, the Department was ranked third (first in
the Research Intensity table published by the Times Higher). In
addition, at the last national assessment of teaching quality, the
Department was rated as "Excellent" and came 2nd in The Complete
University Guide, The Guardian, The Times and The Sunday Times national
league tables by subject.

The Program Specification and Verification Group is led by Professor
Philippa Gardner, and its current focus is on reasoning about JavaScript
and concurrency. The advertised position will target concurrency in
particular (see http://psvg.doc.ic.ac.uk/research/concurrency.html). The
breadth of the REMS project allows for flexibility in the profile of the
candidate, who would work either on the foundations of concurrency
reasoning or on the verification and testing of file systems.

*** Foundations of concurrency reasoning *** Recently, various program
logics based on concurrent separation logic have been developed, by
ourselves and others, with the aim of providing more modular abstract
reasoning about concurrent programs. Our work at Imperial has tackled a
range of problems, including data abstraction (Concurrent Abstract
Predicates), abstract atomicity (the TaDA logic), fault-tolerance and
progress, applying our reasoning to concurrent B-trees, skip lists from
java.util.concurrent, graph algorithms, and the POSIX file system. The
advertised position is suitable for someone interested in such
foundational work on concurrency reasoning and, in particular, its
relationship with respect to linearisability.

*** Verification and testing of file systems *** File-system operations
exhibit complex concurrent behaviour, comprising multiple actions
affecting different parts of the state: typically, multiple atomic reads
followed by an atomic update. The description of the concurrent
behaviour of file-system operations given in the POSIX standard is
unsatisfactory: it is fragmented, contains ambiguities, and is generally
under-specified. We have given a formal concurrent specification of
POSIX file systems and demonstrated scalable reasoning for clients,
combining our ideas about abstract atomicity (TaDA) with refinement. The
advertised position is suitable for someone interested in the
theoretical and practical development of this work on file systems.
Specific tasks include exploring client reasoning, mechanising the
specification and testing real-world implementations by using our
specification as a test oracle, extending our work with fault-tolerance
guarantees, and studying the Network File System, which exhibits weak
consistent behaviours. We expect that some of this work will be done in
collaboration with our colleagues from the University of Cambridge, who
are working on formal methods and systems in the setting of the REMS
project.

We actively encourage applicants who wish to explore their own research
ideas within the scope of the project.  Both our research group and
Imperial as a whole offer many opportunities to help postdocs develop as
independent researchers. Please take a look at our group's web pages and
recent publications (http://psvg.doc.ic.ac.uk/research/concurrency.html)
to see whether the sort of work we do resonates with you, and do not
hesitate to contact me if you are interested in applying for the
position.

Best wishes,
Philippa Gardner
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20160729/a8e6b80b/attachment-0001.html>