advert.md

---
title: Job Announcements
menu_order: 4
---

<h4> Two new postdoc positions at Imperial! </h4> 

We are seeking two outstanding postdocs (one theory, one practice) with
interests in the formal specification and verification of concurrent
and  distributed systems to join the Program Specification and
Verification Group at Imperial.

These positions are funded as part of "REMS: Rigorous Engineering of
Mainstream Systems", a large 6-year EPSRC-funded programme grant between
Cambridge, Edinburgh and Imperial which finishes in 2019.

Concurrent programs are notoriously difficult to get right.  At
Imperial, we have considerable expertise in specifying concurrent
libraries and verifying concurrent programs.  In particular, our
recent work has focussed on the extension of concurrent separation
logic to handle abstraction, abstract atomicity and fault
tolerance. We have applied this reasoning to, for example, concurrent
indexes (B-trees and java.util.concurrent skip lists), the POSIX file
system and an ARIES database recovery algorithm.

Our immediate research aims are  to develop the fundamental principles
underlying reasoning about concurrent systems, to extend the reasoning
to distributed systems, and to test the reasoning on key applications
such as databases, file systems and data centres.

Please see the project web page for more details, and do not
hesitate to contact us if you are interested in one of these postdoc
positions.