@@ -3,7 +3,7 @@ title: One new postdoc position at Imperial College!
---
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.
**\*\*\*Deadline: 18th September \*\*\***
** Deadline: 18th September **
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 <ahref="https://www.cl.cam.ac.uk/~pes20/rems/"target="_blank"> "REMS: Rigorous Engineering of Mainstream Systems"</a>, at the University of Cambridge, University of Edinburgh, and Imperial College London
...
...
@@ -11,9 +11,9 @@ The Department of Computing at Imperial provides a vibrant and stimulating resea
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.
** 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.
** 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.
