Newer
Older
We are seeking two outstanding postdocs (one dominantly theoretical, one
dominantly practical) with strong interests in the formal specification and
verification of concurrent and distributed systems to join the Program
Specification and Verification Group, led by Professor Philippa Gardner,
at Imperial College London.
These positions will be funded as part of <a href="https://www.cl.cam.ac.uk/~pes20/rems/"
target="_blank"> "REMS: Rigorous Engineering of Mainstream Systems"</a>, 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 when it
comes to specification and verification. At
Imperial, we have considerable expertise in specifying concurrent
libraries and verifying concurrent programs. In particular, our
recent work has been 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
underlying reasoning about concurrent systems, to extend the reasoning
to distributed systems, and to test the reasoning on key applications
Please take a look at our [Project web page](/research/concurrency.html) for more details, and do not