Skip to content
Snippets Groups Projects
Commit b460ae42 authored by pmaksimo's avatar pmaksimo
Browse files

Advert

parent a4cd1671
No related branches found
No related tags found
No related merge requests found
...@@ -4,31 +4,34 @@ menu: true ...@@ -4,31 +4,34 @@ menu: true
menu_order: 10 menu_order: 10
--- ---
<h4> Two new postdoc positions at Imperial! </h4> <h4> Two new postdoc positions at Imperial College! </h4>
We are seeking two outstanding postdocs (one theory, one practice) with We are seeking two outstanding postdocs (one dominantly theoretical, one
interests in the formal specification and verification of concurrent dominantly practical) with strong interests in the formal specification and
and distributed systems to join the Program Specification and verification of concurrent and distributed systems to join the Program
Verification Group at Imperial. Specification and Verification Group, led by Professor Philippa Gardner,
at Imperial College London.
These positions are funded as part of "REMS: Rigorous Engineering of These positions will be funded as part of <a href="https://www.cl.cam.ac.uk/~pes20/rems/"
Mainstream Systems", a large 6-year EPSRC-funded programme grant between target="_blank"> "REMS: Rigorous Engineering of Mainstream Systems"</a>, a large 6-year
Cambridge, Edinburgh and Imperial which finishes in 2019. EPSRC-funded programme grant between Cambridge, Edinburgh and Imperial, which
finishes in 2019.
Concurrent programs are notoriously difficult to get right. At Concurrent programs are notoriously difficult to get right when it
comes to specification and verification. At
Imperial, we have considerable expertise in specifying concurrent Imperial, we have considerable expertise in specifying concurrent
libraries and verifying concurrent programs. In particular, our libraries and verifying concurrent programs. In particular, our
recent work has focussed on the extension of concurrent separation recent work has been focussed on the extension of concurrent separation
logic to handle abstraction, abstract atomicity and fault logic to handle abstraction, abstract atomicity, and fault
tolerance. We have applied this reasoning to, for example, concurrent tolerance. We have applied this reasoning to, for example, concurrent
indexes (B-trees and java.util.concurrent skip lists), the POSIX file indexes (B-trees and java.util.concurrent skip lists), the POSIX file
system and an ARIES database recovery algorithm. system, and an ARIES database recovery algorithm.
Our immediate research aims are to develop the fundamental principles Our immediate research aims are to develop the fundamental principles
underlying reasoning about concurrent systems, to extend the reasoning underlying reasoning about concurrent systems, to extend the reasoning
to distributed systems, and to test the reasoning on key applications to distributed systems, and to test the reasoning on key applications
such as databases, file systems and data centres. such as databases, file systems, and data centres.
Please see the project web page for more details, and do not Please take a look at our Project web page for more details, and do not
hesitate to contact us if you are interested in one of these postdoc hesitate to contact us if you are interested in one of these postdoc
positions. positions.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment