<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 a <span class="" style="font-size: 11pt;"> three-year post-doctoral research position available on </span><span class="" style="font-size: 11pt;">`Gillian: Concurrency’, as part of a wider project on the </span>Gillian platform for unified compositional
symbolic reasoning about program correctness and incorrectness. It could turn into a more theoretical or more practical project depending on the strengths of the successful applicant. </div>
<div class="" style="margin: 0cm;">
<div class=""><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 14.666666984558105px;"><br class="">
</span></font></div>
<div class=""><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 14.666666984558105px;">DEADLINE: 15th August 2021, flexible start date in 2022 (or earlier if you wish). </span></font></div>
<div class=""><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 14.666666984558105px;"><br class="">
</span></font></div>
<div class=""><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 14.666666984558105px;">The Gillian project is currently funded by my national fellowship on `Verified Trustworthy Software Specification’ </span></font><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 14.666666984558105px;">and
a large Facebook gift. D</span></font><span class="" style="font-family: Calibri, sans-serif; font-size: 11pt;">etails of this project </span><span class="" style="font-family: Calibri, sans-serif; font-size: 11pt;"> are given below and details about my research
group in general can be </span><span class="" style="font-family: Calibri, sans-serif; font-size: 11pt;">found </span><a href="https://vtss.doc.ic.ac.uk" class="" style="font-family: Calibri, sans-serif; font-size: 11pt;">here</a><span class="" style="font-family: Calibri, sans-serif; font-size: 11pt;">.
I have further flexible funding so please get in touch if the timing for you is not quite right. </span></div>
</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;">
<o:p class="">Best wishes, </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>
<font face="Calibri, sans-serif" class=""><span class="" style="font-size: 14.666666984558105px;"><b class="">Gillian: Concurrency</b></span></font><br class="">
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<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;">
Gillian [1,2] is a multi-language platform for unified compositional symbolic reasoning about program correctness and incorrectness. 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 JavaScript and C, obtaining results on real-world AWS 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 face="Calibri, sans-serif" class=""><span class="" style="font-size: 11pt;">Gillian currently works on sequential programs. This project will</span><span class="" style="font-size: 11pt;"> extend the core of Gillian
with concurrency. A more theoretical project will develop </span></font><span class="" style="font-family: Calibri, sans-serif; font-size: 11pt;">a Gillian instantiation for a small concurrent While language and explore different types of concurrency reasoning
for different types of strong and weak memory models, both theoretically and with Gillian. A more practical project will develop a Gillian instantiation for concurrent Rust, building on the current development of a Gillian instantiation for sequential Rust,
and explore symbolic testing and verification for real-world Rust programs. </span><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 11pt;">The spirit of the group is to get the best fit between people and research, so there is much
flexibility with these projects. </span></font></div>
<div class="" style="margin: 0cm;"><br class="">
</div>
<div class="" style="margin: 0cm;"><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 11pt;">We have recently developed a general infrastructure for the symbolic analysis of event-driven web applications [3]. </span></font><font face="Calibri, sans-serif" class=""><span class="" style="font-size: 11pt;">I
have also worked for many years on the compositional reasoning about concurrent programs, introducing fundamental techniques which underpin modern concurrent separation logics [4,5] and working on
</span></font><span class="" style="font-family: Calibri, sans-serif; font-size: 14.666666984558105px;"> weak consistency models for atomic distributed transactions [6]. </span><span class="" style="font-family: Calibri, sans-serif; font-size: 14.666666984558105px;">Some</span><span class="" style="font-family: Calibri, sans-serif; font-size: 11pt;"> of </span><span class="" style="font-family: Calibri, sans-serif; font-size: 14.666666984558105px;">this experience
will inform the choices for extending </span><span class="" style="font-size: 14.666666984558105px; font-family: Calibri, sans-serif;">Gillian with concurrency, but we will start from the beginning working out what are the right first choices for the project. </span></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;">
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'20. Talks at Rebase at ECOOP/OOPSLAFaceTAV and</div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
Amazon in 2020. </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;">
[2] Gillian, Part 2: Real-world Verification for JavaScript and C, Petar Maksimovic, Sacha-Elie Ayoun, Jose Fragoso Santos and Philippa Gardner, CAV’21, draft available upon request. Talks at <o:p class=""></o:p>Galois and Collège de France in 2021. </div>
<div class="" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">
<br class="">
</div>
<div class="" style="margin: 0cm;"><font face="Calibri, sans-serif" class=""><span style="font-size: 11pt;" class="">[3] A Trusted Infrastructure for Symbolic Analysis of Event-driven Web Applications, Gabriela Sampaio, Jose Fragoso Santos, Petar Maksimovic and
Philippa Gardner, ECOOP</span><span style="font-size: 14.666666984558105px;" class="">’</span><span style="font-size: 11pt;" class="">20. </span></font></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;">
[4] 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;">
[5] TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs, Emanuele D’Osualdo, Azadeh Farzan, Philippa Gardner and Julian Sutherland, TOPLAS 2021, 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;">
[6] Data Consistency in Transactional Storage Systems: a Centralised Approach, Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20.</div>
</body>
</html>