[TYPES/announce] two postdoc positions, reasoning about concurrency and distribution, Imperial

[Gardner, Philippa A]

We are seeking two outstanding postdocs (one theoretical, one more
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.

Two three-year positions will be funded as part of "REMS: Rigorous
Engineering of Mainstream Systems", a 6-year EPSRC-funded programme
grant for £5.6 million between Cambridge, Edinburgh and Imperial,
which finishes in 2019.

It is  not easy to reason about concurrent programs. 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, fault-tolerance and progress.  We have
applied this reasoning to, for example, concurrent indexes (B-trees and
java.util.concurrent skip lists), graph algorithms, the POSIX file
system and an ARIES database recovery algorithm.

Our immediate research goals are: to continue to provide logics for
reasoning about concurrent programs; to develop automated
tools based on our logics; to test the reasoning on key applications
such as databases, file systems and data centres; and to extend the
reasoning to distributed systems.

Please take a look at our Concurrency web page
(http://psvg.doc.ic.ac.uk/research/concurrency.html) for more details
and do not hesitate to contact me at p.gardner at imperial.ac.uk<mailto:p.gardner at imperial.ac.uk> if you
are interested in one of these postdoc positions.

Best wishes,
Philippa Gardner


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20160225/d02c902c/attachment-0001.html>