[TYPES/announce] RA positions, Imperial

[Gardner, Philippa A]

Hello all,

[Sorry for multiple postings.]

I have openings for two post-doctoral research positions in my Verified Software research group at Imperial on `Gillian: Program Correctness and Incorrectness', funded by Facebook, and `Gillian: Coq-Certified Compositional Symbolic Analysis', funded by a national fellowship. Details of these projects are given below.

These positions are for three years. The start date is flexible in these uncertain times, up to September 2021.  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 very good (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.

Philippa

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


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.



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


Gillian: Program Correctness and Incorrectness
Philippa Gardner
Imperial College London

We have introduced Gillian [1], a multi-language platform for compositional symbolic analysis. It 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 the real-world languages C and JavaScript, obtaining results on real-world code that demonstrate the viability of our unified, parametric approach.

Meanwhile, O’Hearn [2] has observed that program correctness for describing the absence of bugs and program incorrectness for describing the presence of bugs are two sides of the same coin. He, Azalea Raad (Imperial) and others [3] have recently introduced incorrectness separation logic for reasoning about program incorrectness, in contrast with Hoare logic and separation logic for reasoning about program correctness. The underlying theory of Gillian resonates with the fundamental ideas of incorrectness logic, suggesting that Gillian has an unexplored potential for reasoning about both program correctness and incorrectness.

Our goal is to establish Gillian as a leading academic platform for integrated analysis of program correctness and incorrectness, by advancing the development of its existing analyses and incorporating the new ideas arising from incorrectness logic. This research position is for three years. It would suit someone with a strong background in formal methods (theory and/or practice), especially someone with experience in program analysis, testing or verification. It is funded by Facebook.

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 the Facebook Testing and Verification Symposium in December, 2020.

[2] Incorrectness Logic, Peter O'Hearn, POPL'20.

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



---------


Gillian: Coq-Certifiction of Compositional Symbolic Analysis
Philippa Gardner
Imperial College London

We have introduced Gillian [1], a multi-language platform for compositional symbolic analysis. It supports three flavours of analysis: whole-program symbolic testing; full verification based on
separation logic; and automatic compositional testing based on bi-abduction. Gillian has been instantiated to the real-world languages C (using the Coq-verified CompCert compiler) and JavaScript (using our own compiler), obtaining results on real-world code that demonstrate
the viability of our unified, parametric approach.

The goal is to provide Coq-certification for the Gillian platform. Gillian is underpinned by a core symbolic execution engine, parametrised by the memory model of the target language, with strong mathematical foundations that unifies symbolic testing and verification. This core is ripe for Coq mechanisation since it has a general correctness result that depends on lemmas associated with particular Gillian instantiations. The challenge is to understand how to link this Coq mechanisation of the core engine to the Gillian platform:  either by replacing the Gillian implementation with extracted Coq code; or by using Gillian to generate proof terms that can be
certified by Coq in order to retain the Gillian optimisations.

This position is for three years, funded by Gardner's UKRI national fellowship. It would suit someone with strong experience with the Coq theorem prover, to enhance the current Coq expertise in the group. In particular, my PhD student Rao Xlaojia is part of the Imperial and
Cambridge team doing WasmCert, a Coq-specification of Wasm [2]. There is also an opportunity to get involved with this WasmCert project if interested.

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 the Facebook Testing and Verification Symposium in December, 2020.

[2] WasmCert-Coq, M. Bodin, P. Gardner, J. Pichon, C. Watt and R. Xiaojia,
https://github.com/WasmCert/WasmCert-Coq
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20201114/9fa56d04/attachment-0001.htm>