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.
You can find more details on Philippa’s research group webpage.
- Nat Karmios
- Sacha-Élie Ayoun
- Philippa Gardner
Proceedings of the 1st ACM International Workshop on Future Debugging Techniques, pp. 1–2
- Petar Maksimović
- Caroline Cronjäger
- Andreas Lööw
- Julian Sutherland
- Philippa Gardner
37th European Conference on Object-Oriented Programming (ECOOP 2023), pp. 19:1–19:27
- Xiaojia Rao
- Aïna Linn Georges
- Maxime Legoupil
- Conrad Watt
- Jean Pichon-Pharabod
- Philippa Gardner
- Lars Birkedal
44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), pp. 151:1–151:25
- Gabriela Sampaio
Ph.D. Thesis, Imperial College London
- Emanuele D’Osualdo
- Azadeh Farzan
- Philippa Gardner
- Julian Sutherland
ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021., vol. 43(4)
- ‘Verified Trustworthy Software Specification, High Integrity Software (HIS) conference’, 2021
- ‘Gillian: a Multi-Language Platform for Compositional Symbolic Analysis’, Collège de France, 2021.
- ‘Gillian: a Multi-Language Platform for Compositional Symbolic Analysis’, Facebook TAV Symposium, 2020.
- ‘Gillian: a Multi-Language Platform for Compositional Symbolic Analysis’, REBASE at OOPSLA and ECOOP, 2020.
- ‘Gillian: a Multi-Language Platform for Compositional Symbolic Analysis’ at Code Mesh V.
- ‘Gillian: a Multi-language Platform for Compositional Symbolic Analysis’ at Amazon Automated Reasoning Symposium, London, UK.
- ‘TADA Live: Compositional Reasoning for the Termination of Fine-grained Concurrent Programs’ at Effective Verification: Static Analysis Meets Program Logics, Lorentz Center Seminar series 2019, Leiden, Netherlands.
- ‘Progress: Scalable Reasoning about Concurrency’, keynote, at Relational and Algebraic Methods in Computer Science (RAMICS 2018), Groningen, Netherlands.
- ‘Trustworthy Software Specification’, keynote, final conference for the DFG priority program ‘Reliably Secure Software Systems (RS3)’, Darmstadt, Germany.
- ‘Verified Trustworthy Software Systems’, invited talk, workshop on Challenges in Industry and Research at the Alan Turing Institute as part of the the Newton Institute programme on Big Proof, London, UK.
- ‘Trustworthy Software Specification: Concurrency’, 28th Hewlett Packard Colloquium on Information Security, RHUL, London;
- ‘A Concurrent Specification of POSIX’, invited talk at Shapiro’s RainbowFS Workshop on Consistency in Distributed Systems, Paris, France.
- ‘Verified Trustworthy Software Systems’, keynote talk at 11th System Safety and Cyber Security Conference, IET, London, UK.
- ‘Scalable reasoning about Concurrent programs’, invited talk and participant at the IFIP WG 1.9/2.15 working group on Verified Software, Montauban, France.
- ‘A Concurrent Specification of POSIX’, invited talk, workshop on Trends in Concurrency Theory (TRENDS 2016), CONCUR, Quebec, Canada.
- ‘A Concurrent Specification of POSIX’, invited talk, Dagstuhl seminar on ‘Synergies among Testing, Verification and Repair for Concurrent Programs’, Dagstuhl, Germany.
- ‘Modern Concurrent Separation Logics’, Plotkin’s 70th birthday celebrations, Edinburgh, UK.
- ‘Research Institute in Automated Program Analysis and Verification’, invited talk, UK Cyber Security Research Conference, London, UK.
- Seminar on Open Problems in Concurrency, organised by ICFP, Bertinoro, Italy.
- ‘Modern Concurrent Separation Logics’, invited tutorial at the Mathematical Foundations of Programming Semantics, Nijmegen, Netherlands.
- ‘Modern Concurrent Separation Logics’, invited tutorial at ECOOP’15, Prague, Czech Republic.
- Workshop on the Certification of High-level and Low-level Programs, Invited talk, Paris, France.
- Workshop on Higher-order Programming with Effects (HOPE 2014), Keynote, associated with ICFP, Gothenburg, Sweden.
- JSTools 2014, Invited talk, associated with ECOOP’14, Uppsala, Sweden.
- Seminar on Open Problems in Concurrency, Bertinoro, organised by ICFP Departmental seminars at Kent, York and Oxford, Bertinoro, Italy.
- Departmental seminars at Kent, York and Oxford, UK.
Teaching and Supervision
I teach the Scalable Software Verification course (fourth-year and M.Sc course)
Undergraduate and M.Sc students
I am keen to supervise undergraduate and M.Sc projects. For available individual and group undergraduate projects, please refer to the projects portal. Or if you are interested in doing your undergraduate/M.Sc project with me, send me an email and we can discuss concrete projects.
I am always keen to hear from prospective PhD students with an interest and strong background in formal software engineering, program verification and reasoning about concurrent programs. Email me if you are interested and attach a CV to your email.
The Imperial College entry requirements page gives you details on academic requirements and other factors taken into account when making a decision on an application. The application process for a PhD is explained on the How to Apply page.
- 2021-2022 Amazon Research Award: Gillian: A Multi-language Platform for Symbolic Testing and Verification, PI, $60,000.
- 2020-2021 Facebook Research gift: Gillian: A Unified Platform for Program Correctness and Incorrectness, PI, $500,000.
- 2018-2023 UKRI Grant, Established Career Fellowship: Verified Trustworthy Software Specification, Fellow, £1.5M.
- 2019 Amazon gift: A Formally Verified Serialisation Module for the AWS Encryption, PI, £100,000.
- 2019—2020 GCHQ grant: Genifer: A Verification and Testing Framework, PI, £75,000, part of the GCHQ funding call for Verified High Assurance Software.
- 2018-2019 Facebook gift: Gillian: A Symbolic Analysis Tool based on Separation Logic, PI, £49,000, awarded following an international competition for Continuous Reasoning that funded 5 projects.
- 2017–2022 EPSRC Grant: Research Institute in Verified Trustworthy Software Systems, PI, £798,000.
- 2015–2016 Facebook Faculty Grant, $40,000.
- 2013–2019 EPSRC Programme Grant: REMS: Rigorous Engineering for Mainstream Systems, CI (Sewell, PI, Cambridge), £1,349,302.
- 2013–2016 EPSRC Grant: Certified Verification of Client-side Web Programs, PI, £627,463.
- 2013–2016 EPSRC and GCHQ Grant: Research Institute in Automated Program Analysis and Verification, PI, £266,461.
- 2010–2016 EPSRC Programme Grant: Resource Reasoning, CI (O’Hearn, PI, UCL), £1,536,661.
- 2006–2010 EPSRC Grant: Smallfoot: Static Assertion Checking for C Programs, CI (O’Hearn, PI, Queen Mary), £330,000.
- 2006–2009 BBSRC Grant: Applying Techniques from Process Algebra to Model Cell Behaviour, PI, £155,146.
- 2004–2007 EPSRC E-science Grant: Dynamic Net Data: Theory and Experiment, PI, £241,438.
- 2003–2006 EPSRC responsive-mode Grant: Spatial Logics for Querying Graphs, PI, £171,916.
- 2002–2004 Microsoft research Grant: Querying Data on the Web, £34,000.
- 1998–2001 EPSRC Grant: Calculi for Interaction: Theory and Experiment, CI (Milner, PI), £279,899.
Awards and Fellowships
- 2018–2023 EPSRC Established Career Fellowship, VeTSpec: Verified Trustworthy Software Specification, Imperial, £1,579,794.
- 2013 President and Rector’s Award for Excellence in Teaching, a prestigious Imperial teaching award.
- 2005–2009 Microsoft Research — Royal Academy of Engineering Senior Research Fellowship, Imperial, £362,272.
- 2007 Rector’s bonus for Research, a prestigious Imperial research award, Imperial, 2007, £10.000.
- 1997-2002 EPSRC Advanced Fellowship, Operational Models of Computation, Cambridge and Imperial, £149,996.
- 1994–1996 The Royal Society of Edinburgh — BP Research Fellowship, Edinburgh, £143,000.
- 1992–1993 Science and Engineering Research Council Postdoctoral Fellowship, Edinburgh, £73,000.
- General Chair of POPL ‘24, the 50th Annual ACM SIGPLAN Symposium on Principles of Programming Languages to be held in London, UK, January 2024
- Fellow of the Royal Academy of Engineering, 2020
- Director of the Research Institute in Verified Trustworthy Software Systems, (VeTSS) 2017-2023
- Chair of the Awards Committee of the BCS Academy of Computing for the Lovelace medal (senior) and the Roger Needham award (mid-career) for Computer Science, 2013-2016
- Director of the Research Institute in Automated Program Analysis and Verification, 2013-2016
- Organiser of the Royal Society Discussion and Scientific meeting on ‘Verified Trustworthy Software Systems’ and associated Specialist Meeting at Imperial College London, 2016
- Lead organiser of the annual UK Workshops on Formal Methods and Tools for Security (FMATS), 2014- 2017, with Markulf Kohlweiss, Mike Gordon, Andy Gordon, Graham Steel and Andy Jackson
- Co-organiser of the annual UK Concurrency Workshop at Imperial, 2015
- Organiser of the annual Introduction to Verification and Testing workshop (INVEST) at Imperial, with Ally Donaldson and Cristian Cadar, which introduce undergraduates and early PhD students to topics in analysis, testing and verification.
- Organiser of Luca Cardelli’s 60th birthday celebrations with Martin Abadi, Andy Gordon and Radu Mardare, 2014
- Editor for the Journal on Foundations and Trends in Programming Languages
- Co-chair of ESOP 2013, DBPL 2009, Chair of CONCUR 2004
- Program Committee member of many major conferences such as POPL, LICS, OOPSLA, ESOP, CONCUR.
- Committee member for Royal Society International Fellowship scheme, 2010-2012
- Member of EPSRC College between 1999-2009