title:One new postdoc position at Imperial College!
---
We are seeking one outstanding postdoc to work on reasoning about concurrent programs.
We are looking for either a theorist to work on the foundations of concurrent reasoning
or a practitioner to work on the specification, verification and testing of file system code.
The position will be with the Program Specification and Verification Group,
led by Professor Philippa Gardner, and will be funded as part of <a href="https://www.cl.cam.ac.uk/~pes20/rems/"
target="_blank"> "REMS: Rigorous Engineering of Mainstream Systems"</a>, a 6-year
EPSRC-funded programme grant for £5.6 million between Cambridge, Edinburgh and Imperial,
which finishes in 2019.
A full advert will follow shortly, but in the meantime, please take a look at our
[Concurrency web page](/research/concurrency.html) for more details
and do not hesitate to contact [Philippa][1] if you are interested in this postdoc
position.
[1]:mailto:p.gardner@imperial.ac.uk
\ No newline at end of file
We are looking to recruit a post-doc 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 theorist to work on the foundations of concurrent reasoning or a theorist/practitioner to work on the verification and testing of file systems.
**Deadline: 18th September**
The position is for 2.5 years (with some flexibility in start date and duration), and will be funded as part of the EPSRC Programme Grant <ahref="https://www.cl.cam.ac.uk/~pes20/rems/"target="_blank"> "REMS: Rigorous Engineering of Mainstream Systems"</a>,`for £5.6M at Cambridge, Edinburgh and Imperial
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 department is consistently recognised by high research ratings. In the 2014 REF assessment, the Department was ranked third (first in the Research Intensity table published by the Times Higher), and was rated as `Excellent' in the previous national assessment of teaching quality.
Our research group works on language specification and program verification, with current work on reasoning about JavaScript and concurrency. This position focuses particularly on [concurrency.](/research/concurrency.html) The breadth of the REMS project allows for some flexibility in the profile of the candidate, to 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, to provide 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, skiplists from java.util.concurrent, graph algorithms and the POSIX file system. Our position is suitable for someone interested in such foundational work on concurrency reasoning and, in particular, its connections and differences with 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 POSIX standard’s description of the concurrent behaviour of file-system operations is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We have given a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients, combining our ideas about abstract atomicity (TaDA) with refinement. Our position is suitable for someone interested in the theoretical and practical development of this file-system work.
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 Network File System which exhibits weak consistent behaviours. We expect some of this work will be done in collaboration with our Cambridge formal methods and systems colleagues on 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 have a look at our group's [web pages and recent publications](/research/concurrency.html) to see whether the sort of work we do excites you, and contact [me][1] if you are interested in applying for the position.
