[TYPES/announce] PhD position in the analysis of concurrent or distributed programs, Imperial

[Gardner, Philippa A]

Hello all,

[Apologies for multiple postings.]

I am looking for a PhD student who is interested in the analysis of concurrent or distributed programs, start date in October 2021. A summary of possible research projects is given below and details about my research group can be found here<https://vtss.doc.ic.ac.uk>.

The deadline to apply for a PhD position in the Department is **19th March 2021**. A successful UK student will probably be funded through the standard Departmental competition for funds. A successful EU/overseas student will probably be funded by a combination of Departmental funding and my funding. In particular, I have additional funding which means that the EU/overseas students are able to go into the same competition for funding as the UK students.

Given these uncertain times, we will assess the situation about whether it is necessary to start the position remotely nearer the time. The good news is that accommodation rents are currently low due to covid, with people in my group recently getting some excellent accommodation, and so it is actually quite a good time to come to London.

Please do not hesitate to contact me directly if interested, cc’ing my administrator Teresa Carbajo Garcia, cc'd.

Best wishes,
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.
———————————————————————————————————————————

POSSIBLE PROJECTS

Gillian: Concurrency

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

We have an ambitious project 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.

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210307/94801f85/attachment-0001.htm>