[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Hello all,
[Apologies for multiple postings.]
I have a three-year post-doctoral research position available on `Gillian:
Concurrency’, as part of a wider project on the 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.
DEADLINE: 15th August 2021, flexible start date in 2022 (or earlier if you
wish).
The Gillian project is currently funded by my national fellowship on `Verified
Trustworthy Software Specification’ and a large Facebook gift. Details of this
project are given below and details about my research group in general can be
found here<https://vtss.doc.ic.ac.uk>. I have further flexible funding so
please get in touch if the timing for you is not quite right.
If you are interested, please do not hesitate to contact me, cc’ing my
administrator Teresa Carbajo Garcia,
[email protected]<mailto:[email protected]>.
Best wishes,
Philippa
---------------------------------------------------------------------------------------
Professor Philippa Gardner FREng
Department of Computing
Imperial College
180 Queen’s Gate
London
SW7 2AZ
Your working day may not be the same as mine. Please do not feel
obliged to reply to this email outside your normal working hours.
---------------------------------------------------------------------------------------
Gillian: Concurrency
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.
Gillian currently works on sequential programs. This project will extend the
core of Gillian with concurrency. A more theoretical project will develop 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. The spirit of
the group is to get the best fit between people and research, so there is much
flexibility with these projects.
We have recently developed a general infrastructure for the symbolic analysis
of event-driven web applications [3]. 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 weak consistency models for atomic distributed transactions [6]. Some of
this experience will inform the choices for extending Gillian with concurrency,
but we will start from the beginning working out what are the right first
choices for the project.
References
[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
Amazon in 2020.
[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 Galois and Collège de France in 2021.
[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] 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.
[6] Data Consistency in Transactional Storage Systems: a Centralised Approach,
Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20.
