[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
