[TYPES/announce] three-year postdoc position on verifying concurrent programs

[Gardner, Philippa A]

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,
t.carbajo-garcia at imperial.ac.uk<mailto:t.carbajo-garcia at imperial.ac.uk>.

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210714/b09cadcd/attachment-0001.htm>