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.
*** Applications now closed ***
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
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.
*** 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 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.