[TYPES/announce] RA position, Imperial, symbolic analysis, concurrency or distribution

[Gardner, Philippa A]

Hi all,

Sorry for multiple postings.

I would like to announce the availability of an RA position in my
research group at Imperial College London. This position is initially
for two years with an option to extend in future.  My funding from a
research fellowship is flexible so the start date can be flexible in
these uncertain times, in the academic year starting September 2020.
I also expect to have further funding available over the next year.  If
interested, please contact me by **15th June**, just so that I have an
understanding of who might be interested in either this position or a
future position.

I give a description of some potential projects below, focussing on
symbolic analysis, concurrency and distribution.

1.  Gillian: a multi-language platform for compositional symbolic
analysis

My group has recently introduced Gillian (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. I would especially like to recruit
someone interested in extending Gillian with concurrency or
underpinning Gillian with Coq-certification.

2. Concurrency

My 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.

My group has recently begun to work on weak consistency models for
distribution, developing an interleaving operational semantics for
client-observational behaviour of atomic transactions (ECOOP’20).

I would be interested in 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 which connect with program logics for
concurrency and weak memory.

-----

A successful candidate is likely to have a strong record of research
in programme languages, analysis or verification. They will join my
Verified Software group at Imperial. Current and former RAs and PhD
students from this group include Brotherston (UCL academic), Calcagno
(Imperial academic then Monoidics start-up then Facebook), Maffeis
(Imperial academic), Naudziuniene (Infer at Facebook), Ntzik (systems
R&D at Amadeus), Raad (Imperial academic), Smith (Pivotal Software
Inc) and Villard (Infer at Facebook). We have thriving interactions
with the tech companies in London, especially with Facebook and Amazon
who fund my research.

If you are interested in joining my group and want to learn more about
the various projects, please contact me directly at
p.gardner at imperial.ac.uk<mailto:p.gardner at imperial.ac.uk>.

Best wishes,
Philippa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20200517/1d0899bb/attachment-0001.html>