[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Hello all,
[Apologies for multiple postings.]
I have an opening for a post-doctoral research position at Imperial on
`Gillian: Concurrency', funded by a national fellowship: details of the project
are given below; details about my research group can be found
here<https://vtss.doc.ic.ac.uk>.
[I have flexible funding and so also include brief descriptions of my more
theoretical work on reasoning about concurrent and distributed programs in case
it is of interest.]
The position is for three years. The start date is flexible in these uncertain
times, but two good times are September 2021 and January 2022. It is possible
to start the positions remotely, although we are able to meet at Imperial when
necessary so it might make sense to be in London. In fact, accommodation rents
are currently low (due to covid) so it is actually quite a good time to come to
London.
If you are interested, please do not hesitate to contact me, cc’ing my
administrator Teresa Carbajo Garcia,
[email protected]<mailto:[email protected]>.
Philippa
---------------------------------------------------------------------------------------
Professor Philippa Gardner FREng
Department of Computing
Imperial College
180 Queen’s Gate
London
SW7 2AZ
Your working day may not be the same as mine. Please do not feel
obliged to reply to this email outside your normal working hours.
---------------------------------------------------------------------------------------
THE PROJECT
Gillian: Concurrency
Philippa Gardner
Imperial College London
Gillian [1,1a] is a multi-language platform for compositional symbolic
analysis. It currently supports three flavours of analysis: whole-program
symbolic testing; full verification based on separation logic; and automatic
compositional testing based on bi-abduction. It is underpinned by a core
symbolic execution engine, parametric on the memory model of the target
language, with strong mathematical foundations that unifies symbolic testing
and verification. Gillian has been instantiated to C and JavaScript, obtaining
results on real-world code that demonstrate the viability of our unified,
parametric approach.
The ambitious aim is to design and implement Concurrent Gillian. It involves:
changing the core of Gillian to handle concurrency; developing a Gillian
instantiation for a small concurrent While language to explore different types
of concurrency reasoning; developing a Gillian instantiation for concurrent
Rust which will build on the current development of a Gillian instantiation for
sequential Rust; and exploring symbolic testing and verification for real-world
Rust programs. We are also about to begin projects on `Gillian: Program
Correctness and Incorrectness', funding by Facebook, and `The Coq-certification
of Gillian'. The spirit of the group is to get the best fit between people and
research, so there is much flexibility with working on these other projects as
well.
OTHER PROJECTS ON CONCURRENCY AND DISTRIBUTION
Concurrency
We have worked for many years on the compositional reasoning about concurrent
programs, introducing fundamental techniques which underpin modern concurrent
separation logics [2,2a]: logical abstraction; logical atomicity; and logical
environment liveness properties. We have applied our reasoning to verify some
of the most advanced concurrent algorithms in the literature. There are several
suitable PhD projects associated with this work: for example, continuing the
work on the foundational theory; applying the work to real-world libraries;
developing prototype analysis tools; or using the Coq-focused Iris project,
whose foundations use some of our theory.
Distribution
We have recently begun to work on weak consistency models for distribution,
developing an interleaving operational semantics for client-observational
behaviour of atomic transactions [5]. Possible PhD projects include: creating a
program logic for distributed atomic transactions (our original motivation for
the work) inspired by our previous work on program logics for concurrency; or
further developing the operational semantics with the aim to provide prototype
tools for proving robustness results and discovering litmus tests.
References
[1] Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose
Fragoso Santos, Petar Maksimovic, Sacha-Elie Ayoun and Philippa Gardner,
PLDI'2020. Part 2 on verification and bi-abduction is being written now. We
have given a talk on Gillian at the conference Rebase, associated with
ECOOP/OOPSLA, in November 2020, and at Facebook's Testing and Verification
Symposium (FaceTAV), in December 2020.
[1a] Gillian Verification for JavaScript and C, Petar Maksimovic, Sacha-Elie
Ayoun, Jose Fragoso Santos and Philippa Gardner, submitted, draft available
upon request.
[2] A Perspective on Specifying and Verifying Concurrent Modules, Thomas
Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner, Journal of Logical
and Algebraic Methods in Programming, 2018.
[2a] TaDA Live: Compositional Reasoning for Termination of Fine-grained
Concurrent Programs, Emanuele D’Osualdo, Azadeh Farzan, Philippa Gardner and
Julian Sutherland, submitted for journal publication 2020, draft available upon
request.
[3] Data Consistency in Transactional Storage Systems: a Centralised Approach,
Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20.
