VOOZH about

URL: https://www.doc.ic.ac.uk/~pg/

⇱ Philippa Gardner

Biography

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 focusses 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.

Research Group

You can find more details on Philippa’s research group webpage.

Full Bibliography

Publications and PhD Theses

  1. File Info

    Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees

    • Nat Karmios
    • Sacha-Élie Ayoun
    • Philippa Gardner

    Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2026

  2. File Info

    Designing and Maintaining an Efficient WebAssembly Mechanisation

    • Xiaojia Rao

    Ph.D. Thesis, Imperial College London, 2025

  3. File Info

    Compositional Symbolic Execution for the Next 700 Memory Models

    • Andreas Lööw
    • Seung Hoon Park
    • Daniele Nantes-Sobrinho
    • Sacha-Élie Ayoun
    • Opale Sjöstedt
    • Philippa Gardner

    OOPSLA 2025

  4. File Info

    A Hybrid Approach to Semi-automated Rust Verification

    • Sacha-Élie Ayoun
    • Xavier Denis
    • Petar Maksimović
    • Philippa Gardner

    PLDI 2025

  5. File Info

    Gillian: Foundations, Implementation, and Applications of Compositional Symbolic Execution

    • Sacha-Élie Ayoun

    Ph.D. Thesis, Imperial College London, 2025

Full Bibliography

Invited Talks

2021

  • ‘Verified Trustworthy Software Specification, High Integrity Software (HIS) conference’, 2021
  • ‘Gillian Verification for JavaScript and C’, Galois, 2021.
  • ‘Gillian: a Multi-Language Platform for Compositional Symbolic Analysis’, Collège de France, 2021.

2020

  • ‘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.

2019

  • ‘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.

2018

  • ‘Progress: Scalable Reasoning about Concurrency’, keynote, at Relational and Algebraic Methods in Computer Science (RAMICS 2018), Groningen, Netherlands.
  • ‘JaVerT 2.0: JavaScript Verification and Testing Framework’, invited talk at Principles and Practice of Declarative Programming (PPDP 2018), Frankfurt, Germany.

2017

  • ‘Verification and Testing for JavaScript’, invited talk at the first Facebook Testing and Verification Symposium, Facebook, London, UK.
  • ‘Trustworthy Software Specification’, keynote, final conference for the DFG priority program ‘Reliably Secure Software Systems (RS3)’, Darmstadt, Germany.
  • ‘JaVerT: The JavaScript Verification Toolchain’, keynote, International Conference on Automated Reasoning (CADE), Gothenburg, Sweden.
  • ‘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.
  • ‘Towards Trustworthy Verification of JavaScript’, invited talk at the Emerging technologies session, TC39: ECMAScript Task group standards committee meeting, New York, USA.
  • ‘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.
  • ‘Tractable Verification of JavaScript Programs’, keynote talk at FSEN’17, Tehran, Iran.
  • ‘Understanding and Verifying JavaScript Programs’, UPMC Informatics Colloquium (Distinguished Seminar Series), Paris, France.
  • ‘Tractable Verification of JavaScript Programs’ invited talk on JSVerify at the workshop on Principles in Practice, POPL’17, Paris, France.

2016

  • ‘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.
  • ‘An Intermediate Language and Compiler for JavaScript Verification’, invited talk at JSTools workshop associated with ECOOP’16, Rome, Italy.
  • ‘JavaScript and Concurrency Verification’, invited talk, the first workshop on DeepSpec: The Science of Deep Specification, Princeton, USA (with Petar Maksimovic).
  • ‘A Concurrent Specification of POSIX’, invited talk, Dagstuhl seminar on ‘Synergies among Testing, Verification and Repair for Concurrent Programs’, Dagstuhl, Germany.
  • ‘Understanding and Verifying JavaScript Programs’, talk at the Royal Society Discussion and Scientific meeting on ‘Verified trustworthy software systems’, Royal Society, London, UK.
  • ‘Modern Concurrent Separation Logics’, Plotkin’s 70th birthday celebrations, Edinburgh, UK.
  • ‘Understanding and Verifying JavaScript Programs’, 30th Anniversary of LFCS, Edinburgh, UK.

2015

  • ‘Understanding and Verifying JavaScript programs’, invited talk, Google EU Compiler Summit’15, Munich, Germany.
  • ‘Understanding and Verifying JavaScript programs’, invited talk, Departmental seminar at Cambridge, 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.
  • ‘A Trusted Mechanised Specification of JavaScript: One Year On’, keynote talk at CAV’15, San Francisco, USA.
  • ‘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.

2014

  • 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.
  • ‘A Trusted Mechanised Specification of the JavaScript Standard’, Departmental Seminar, Oxford University, UK.
  • 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.

Postgraduate Students

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.

Grants

  • 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.

Activities

Contact

Philippa Gardner

  • pgxxdoc.ic.ac.uk (substitute xx for @)
  • +44 (0)20 7594 8292

Teresa Ng

Program Manager

Address

  • Department of Computing
    180 Queen's Gate
    South Kensington Campus
    Imperial College London
    SW7 2AZ