[TYPES/announce] PhD positions available

[Gardner, Philippa A]

Hello all,

[Sorry for multiple postings.]

I am looking for one or two PhD students, start date in October 2021, to join my Verified Software research group<https://www.doc.ic.ac.uk/~pg/#research-group>. A summary of  possible research projects is given below.

The deadlines to apply for a PhD position in the Department are 8th January 2021 and 19th March 2021. The Department advises all students requiring funding to apply by the January deadline, although there may still be some funding available for applications received after January. Further details can be found here<http://www.imperial.ac.uk/computing/prospective-students/phd/>.  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.

Please do not hesitate to  contact me directly  if interested, cc’ing my administrator Teresa Carbajo Garcia, t.carbajo-garcia at imperial.ac.uk<mailto:t.carbajo-garcia at imperial.ac.uk>.

Best wishes,
Philippa

Research in the Verified Software Group, Imperial

My group is involved with a wide range of theoretical and practical projects on symbolic testing and verification in particular, and on formal methods in general. They are summarised below.  All have many opportunities for PhD projects.

Gillian: a multi-language platform for compositional symbolic analysis

The Verified Software Group has recently introduced Gillian [1], 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.

Possible projects include: incorporating ideas from incorrectness separation logic to Gillian [2]; extending Gillian with events and concurrency [3]; underpinning Gillian with Coq certification;
instantiating Gillian with C (we have just started, [1]) and Rust (we have hardly begun); and using the Gillian instantiations for symbolic testing and verification of real-world programs.

Concurrency

The Verified Software Group has worked on compositional reasoning about concurrent programs, introducing fundamental techniques underpinning modern concurrent separation logics [4]: logical abstraction; logical atomicity; and logical environment liveness
properties. We have applied our reasoning to verify some of the most advanced concurrent algorithms.

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, whose foundations use some of our theory.

Distribution

The Verified Software Group has recently begun to work on weak consistency models for distribution, developing an interleaving operational semantics for client-observational behaviour of atomic transactions [5].

We would be interested in finding someone to work in this area: for example, developing further the operational semantics and providing prototype tools to prove robustness results and discover litmus tests; or creating a program logic for distributed atomic transactions (our original motivation for the work) inspired by our previous work on program logics for concurrency.

References

[1] Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose Fragoso Santos, Peter Maksimovic, Sacha-Elie Ayoun and Philippa Gardner, PLDI'2020. Part 2 on verification and bi-abduction is being written now! We are giving a talk on Gillian at the conference Rebase,
associated with ECOOP and OOPSLA, on 16th and 17th November, and at  Facebook's Testing and Verification Symposium (FaceTAV),  in December 2020.

[2] Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad (Imperial), Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn and Jules Villard, CAV'20.

[3] A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications, Gabriela Sampaio, Jose Fragoso Santos, Petar Maksimovic and Philippa Gardner, ECOOP'20

[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

[5] Data Consistency in Transactional Storage Systems: a Centralised Approach, Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20



----------------------------------------------------------------------------------------


Professor Philippa Gardner
Department of Computing
Imperial College
180 Queen’s Gate
London
SW7 2AZ


My working day may not be the same as yours.  Please do not feel
obliged to reply to this email outside your normal working hours.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20201113/9baa3fb7/attachment-0001.htm>