advert

advert.md

+---
+title: Job Announcements
+menu_order: 4
+---
+
+<div class="card card-block">
+
+<h4 class="card-title"> 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.
+
+</div>