From 001337cc7fda24a342e5d22e6416215519b7ed9b Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Tue, 26 Jul 2016 13:52:14 +0100 Subject: [PATCH] Update 2016-02-18-advert.md --- _posts/2016-02-18-advert.md | 35 ++++++++++------------------------- 1 file changed, 10 insertions(+), 25 deletions(-) diff --git a/_posts/2016-02-18-advert.md b/_posts/2016-02-18-advert.md index 5a5fafb..2dc5f3e 100644 --- a/_posts/2016-02-18-advert.md +++ b/_posts/2016-02-18-advert.md @@ -1,34 +1,19 @@ --- -title: Two new postdoc positions at Imperial College! +title: One new postdoc position at Imperial College! --- -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. +We are seeking one outstanding postdoc to work on reasoning about concurrent programs. +We are looking for either a theorist to work on the foundations of concurrent reasoning +or a practitioner to work on the specification, verification and testing of file system code. -These positions will be funded as part of <a href="https://www.cl.cam.ac.uk/~pes20/rems/" +The position will be with the Program Specification and Verification Group, +led by Professor Philippa Gardner, and 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 6-year EPSRC-funded programme grant for £5.6 million 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 -system and an ARIES database recovery algorithm. - -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. - -Please take a look at our [Concurrency web page](/research/concurrency.html) for more details -and do not hesitate to contact [Philippa][1] if you are interested in one of these postdoc -positions. +A full advert will follow shortly, but in the meantime, please take a look at our +[Concurrency web page](/research/concurrency.html) for more details +and do not hesitate to contact [Philippa][1] if you are interested in this postdoc +position. [1]: mailto:p.gardner@imperial.ac.uk \ No newline at end of file -- GitLab