The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

Hello everyone,

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 Philippa at 
p.gardner AT imperial.ac.uk
 if
you are interested in one of these postdoc positions.

Best wishes,
Petar Maksimovic

Petar Maksimovic, Ph.D.
Research Fellow
Department of Computing
Imperial College London
South Kensington Campus
London SW7 2AZ
Email: 
p.maksimovic AT imperial.ac.uk