Summary
Philippa Gardner is a professor in the Department of Computing at Imperial College London and has a UK Research and Innovation Established Fellowship from 2018-2023.
Her research focuses on program specification and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, and is currently developing the Gillian platform for building symbolic analysis tools for real-world programming languages such as C and JavaScript, which unifies classical symbolic execution, semi-automatic verification based on separation logic, and automatic compositional testing based on bi-abduction.
Gardner completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship at Imperial, 2005--2009. In 2020 she was elected a Fellow of the Royal Academy of Engineering.
Philippa was the director of the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC, 2017-2023. Philippa is the general Chair for POPL ‘24, the 50th Annual ACM SIGPLAN Symposium on Principles of Programming Languages to be held in London, in January 2024 and was also an organiser of the Isaac Newton Institute six-week summer programme on `Verified Software’, 2022.
Publications
Journals
D'Osualdo E, Sutherland J, Farzan A, et al., 2021, TaDA Live: compositional reasoning for termination of fine-grained concurrent programs, Acm Transactions on Programming Languages and Systems, Vol:43, ISSN:0164-0925
Conference
Karmios N, Ayoun S-É, Gardner P, 2023, Symbolic debugging with Gillian, DEBT '23: 1st ACM International Workshop on Future Debugging Techniques, ACM, Pages:1-2
Maksimovic P, Cronjäger C, Loow A, et al., 2023, Exact separation logic: towards bridging the gap between verification and bug-finding, ECOOP 2023, Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages:19:1-19:27, ISSN:1868-8969
Rao X, Georges AL, Legoupil M, et al., 2023, Iris-Wasm: robust and modular verification of WebAssembly programs, PLDI 2023, Association for Computing Machinery (ACM), Pages:1096-1120, ISSN:2475-1421