first attempt

_posts/2020-06-18-advert.md

+---
+title: Post-doc Position(s) Available
+---
+
+There is an opening in Verified Software Group for at least one
+post-doctoral researcher. This position is initially
+for two years with an option to extend in future. The funding from
+Philippa's EPSRC Fellowship allows for a flexible start date in
+these uncertain times, in the academic year starting September 2020.
+Further funding is expected to be available over the next year.  If
+interested, please contact [Philippa](mailto:p.gardner@imperial.ac.uk?subject=[Inquiry]%20Post-doctoral%20Position)
+directly as soon as possible.
+
+A successful candidate is likely to have a strong record of research
+in program analysis, testing, or verification. Former
+RAs and PhD students from the Verified Software group include
+Brotherston (UCL academic), Calcagno (Imperial academic, then
+Monoidics start-up, then Facebook), Maffeis
+(Imperial academic), Naudziuniene (Facebook Infer), Ntzik (Amadeus R&D),
+Raad (Imperial academic), Smith (Pivotal Software
+Inc.) and Villard (Facebook Infer). We have thriving interactions
+with the tech companies in London, especially Facebook and Amazon,
+who fund part of the group's research.
+
+Several potential projects are listed below, focussing on
+symbolic analysis, concurrency and distribution.
+
+1. Gillian: a multi-language platform for compositional symbolic
+analysis
+
+The Verified Software Group has recently introduced
+[Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html) (PLDI'20),
+supporting three flavours of analysis: symbolic testing, full verification and
+automatic compositional testing, unified by a common symbolic
+execution engine that is parametric on the memory model of the target
+language. We instantiate Gillian to the real-world languages C and
+JavaScript, obtaining results on real-world code that demonstrate the
+viability of our unified, parametric approach.
+
+There are many possible projects. We would especially like to recruit
+someone interested in extending Gillian with concurrency or
+underpinning Gillian with Coq-certification.
+
+2. Concurrency
+
+The Verified Software Group has worked on compositional reasoning about concurrent
+programs, introducing fundamental techniques underpinning modern
+concurrent separation logics: logical abstraction (CAP logic), logical
+atomicity (TaDA Safety) and logical environment liveness properties
+(TaDA Live). We have applied our reasoning to, for example, algorithms
+for manipulating concurrent B-trees, skip lists from
+java.util.concurrent, graph algorithms and the POSIX file system.
+
+There is still much to understand: for example, working with the
+fundamental theory; applying the work to real-world libraries;
+developing prototype analysis tools; or moving to the Coq-focused Iris
+project, which uses much of our foundational theory.
+
+3. Distribution.
+
+The Verified Software Group recently began to work on weak consistency models for
+distribution, developing an interleaving operational semantics for
+client-observational behaviour of atomic transactions (ECOOP’20).
+
+We would be interested in finding someone to work in this area: for example,
+developing further the operational semantics and providing prototype
+tools for proving robustness results or discovering litmus tests; or
+introducing program logics that connect with program logics for
+concurrency and weak memory.