<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Hello all,<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
[Apologies for multiple postings.]<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
I have an opening for a post-doctoral research position at Imperial on <span class="" style="font-size: 11pt;">`Gillian: Concurrency', funded by a national fellowship: details of </span><span class="" style="font-size: 11pt;">the project are given below; details
about my research group can be </span><span class="" style="font-size: 11pt;">found </span><a href="https://vtss.doc.ic.ac.uk" class="" style="font-size: 11pt;">here</a><span class="" style="font-size: 11pt;">.</span></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
[I have flexible funding and so also include brief descriptions of my <span class="" style="font-size: 11pt;">more theoretical work on reasoning about concurrent and distributed </span><span class="" style="font-size: 11pt;">programs in case it is of interest.]</span></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<span class="" style="font-size: 11pt;"><br class="">
</span></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
The position is for three years. The start date is flexible in these <span class="" style="font-size: 11pt;">uncertain times, but two good times are September 2021 and January </span><span class="" style="font-size: 11pt;">2022. It is possible to start the
positions remotely, although we are </span><span class="" style="font-size: 11pt;">able to meet at Imperial when necessary so it might make sense to be </span><span class="" style="font-size: 11pt;">in London. In fact, accommodation rents are currently low
(due </span><span class="" style="font-size: 11pt;">to covid) so it is actually quite a good time to come to London.</span></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
If you are interested, please do not hesitate to contact me, cc’ing my <span class="" style="font-size: 11pt;">administrator Teresa Carbajo Garcia,</span><span class="" style="font-size: 11pt;"> </span></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<a href="mailto:t.carbajo-garcia@imperial.ac.uk" class="" style="font-size: 11pt;">t.carbajo-garcia@imperial.ac.uk</a><span class="" style="font-size: 11pt;">.</span></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Philippa<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
---------------------------------------------------------------------------------------<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Professor Philippa Gardner FREng<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Department of Computing<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Imperial College <o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
180 Queen’s Gate<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
London<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
SW7 2AZ<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Your working day may not be the same as mine. Please do not feel<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
obliged to reply to this email outside your normal working hours.<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
---------------------------------------------------------------------------------------<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
THE PROJECT<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Gillian: Concurrency<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Philippa Gardner<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Imperial College London<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
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.<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
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. <o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
OTHER PROJECTS ON CONCURRENCY AND DISTRIBUTION<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Concurrency<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
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.<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Distribution<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
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. <o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
References<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
[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.<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
[1a] Gillian Verification for JavaScript and C, Petar Maksimovic, Sacha-Elie Ayoun, Jose Fragoso Santos and Philippa Gardner, submitted, draft available upon request.<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
[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.<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
[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.<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""></o:p></div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
[3] Data Consistency in Transactional Storage Systems: a Centralised Approach, Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20.</div>
</body>
</html>