diff --git a/_posts/2016-07-26-advert.md b/_posts/2016-07-26-advert.md index 3c254a288c2732b44572b9e4fb05bf4b579ed232..5a58fdfd524fc0a8f65cc70fae26c68bae11c1b9 100644 --- a/_posts/2016-07-26-advert.md +++ b/_posts/2016-07-26-advert.md @@ -1,23 +1,23 @@ --- title: One new postdoc position at Imperial College! --- -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. +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 \*\*\* ** -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 <a href="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 +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 <a href="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 -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. +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. -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. +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, 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. +** \*\*\* 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 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. +** \*\*\* 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. -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. +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 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. +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](/research/concurrency.html) to see whether the sort of work we do resonates with you, and do not hesitate to [contact me][1] if you are interested in applying for the position. Philippa Gardner