There is an opening for at least one post-doctoral researcher in the Verified Software Group led by Professor Philippa Gardner. 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 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.
Gillian: a multi-language platform for compositional symbolic analysis
There are many possible projects. We would especially like to recruit someone interested in extending Gillian with concurrency or underpinning Gillian with Coq-certification.
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.
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.