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