diff --git a/advert.md b/advert.md index c6d0de9760a491dffbc85c58c4f9e0f58e50de57..c599aaca847ee7bcb040af5f6672fea4c3ca4a2a 100644 --- a/advert.md +++ b/advert.md @@ -4,31 +4,34 @@ menu: true 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 -interests in the formal specification and verification of concurrent -and distributed systems to join the Program Specification and -Verification Group at Imperial. +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 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. +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. 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 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 +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 -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 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 positions.