Photo of Philippa Gardner
  Webpage   pg@doc.ic.ac.uk

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.

Philippa directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC, 2017-2022. She is an organiser of the Isaac Newton Institute six-week summer programme on `Verified Software’, 2022. In 2020 she was elected a Fellow of the Royal Academy of Engineering.

Group Publications

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

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

  2. Compositional Symbolic Execution for the Next 700 Memory Models

    OOPSLA 2025

  3. A Hybrid Approach to Semi-automated Rust Verification

    PLDI 2025

  4. Progressful Interpreters for Efficient WebAssembly Mechanisation

    POPL 2025

  5. Matching Plans for Frame Inference in Compositional Reasoning

    ECOOP 2024

  6. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

    ECOOP 2024

  7. Bringing the WebAssembly Standard up to Speed with SpecTec

    PLDI 2024

  8. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding

    ECOOP 2023

  9. Symbolic Debugging with Gillian

    Future Debugging Techniques (DEBT) @ ECOOP 2023

  10. Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

    PLDI 2023

  11. Two Mechanisations of WebAssembly 1.0

    Formal Methods (FM) 2021

  12. TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

    Transactions on Programming Languages and Systems (TOPLAS) 2021

  13. Gillian, Part II: Real-World Verification for JavaScript and C

    CAV 2021

  14. Data Consistency in Transactional Storage Systems: a Centralised Approach

    ECOOP 2020

  15. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

    ECOOP 2020

  16. Gillian, Part I: A Multi-language Platform for Symbolic Execution

    PLDI 2020

  17. A Program Logic for First-Order Encapsulated WebAssembly

    ECOOP 2019

  18. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

    POPL 2019

  19. Skeletal Semantics and their Interpretations

    POPL 2019

  20. JaVerT: JavaScript Verification and Testing Framework: Invited Talk

    Principles and Practice of Declarative Programming (PPDP) 2018

  21. Symbolic Execution for JavaScript

    Principles and Practice of Declarative Programming (PPDP) 2018

  22. JaVerT: JavaScript Verification Toolchain

    POPL 2018

  23. A Perspective on Specifying and Verifying Concurrent Modules

    Journal of Logical and Algebraic Methods in Programming 2018

  24. A Concurrent Specification of POSIX File Systems

    ECOOP 2018

  25. Verified Trustworthy Software Systems

    Philosophical Transactions of the Royal Society of London A 2017

  26. Towards Logic-based Verification of JavaScript Programs

    Conference on Automated Deduction (CADE) 2017

  27. Abstract Specifications for Concurrent Maps

    ESOP 2017

  28. Verifying Concurrent Graph Algorithms

    Asian Symposium on Prograaming Languages and Systems (APLAS) 2016

  29. DOM: Specification and Client Reasoning

    Asian Symposium on Programming Languages and Systems (APLAS) 2016

  30. Modular Termination Verification for Non-blocking Concurrency

    ESOP 2016

  31. Fault-tolerant Resource Reasoning

    Asian Symposium on Programming Languages and Systems (APLAS) 2015

  32. Reasoning about the POSIX File System: Local Update and Global Pathnames

    OOPSLA 2015

  33. Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)

    Mathematical Foundations of Programming Semantics (MFPS) 2015

  34. CoLoSL: Concurrent Local Subjective Logic

    ESOP 2015

  35. A Trusted Mechanised Specification of JavaScript: One Year On

    CAV 2015

  36. Abstract Local Reasoning for Concurrent Libraries: Mind the Gap

    Mathematical Foundations of Programming Semantics (MFPS) 2014

  37. TaDA: A Logic for Time and Data Abstraction

    ECOOP 2014

  38. Local Reasoning for the POSIX File System

    ESOP 2014

  39. A Trusted Mechanised JavaScript Specification

    POPL 2014

  40. JuS: Squeezing the Sense out of JavaScript Programs

    Tools for JavaScript Analysis (JSTools) @ ECOOP 2013

  41. Views: Compositional Reasoning for Concurrent Programs

    • Thomas Dinsdale-Young
    • Lars Birkedal
    • Philippa Gardner
    • Matthew J. Parkinson
    • Hongseok Yang

    POPL 2013

  42. Processes in Space

    Theoretical Computer Science 2012

  43. Towards a Program Logic for JavaScript

    POPL 2012

  44. A Simple Abstraction for Complex Concurrent Indexes

    OOPSLA 2011

  45. Abstract Local Reasoning for Program Modules

    Algebra and Coalgebra in Computer Science (CALCO) 2011

  46. Report on the EDBT/ICDT 2010 workshop on updates in XML

    • Michael Benedikt
    • Daniela Florescu
    • Philippa Gardner
    • Giovanna Guerrini
    • Marco Mesiti
    • Emmanuel Waller

    Special Interest Group on Management of Data (SIGMOD) 2010

  47. Resource Reasoning about Mashups

    Verified Software: Theories, Tools and Experiments (VSTTE) 2010

  48. Locality Refinement

    Verified Software: Theories, Tools and Experiments (VSTTE) 2010

  49. Abstraction and Refinement for Local Reasoning

    Verified Software: Theories, Tools and Experiments (VSTTE) 2010

  50. Concurrent Abstract Predicates

    • Thomas Dinsdale-Young
    • Mike Dodds
    • Philippa Gardner
    • Matthew J. Parkinson
    • Viktor Vafeiadis

    ECOOP 2010

  51. Processes in Space

    Programs, Proofs, Processes @ Computability in Europe (CiE) 2010

  52. Adjunct Elimination in Context Logic for Trees

    Information and Computation 2010

  53. Reasoning About Client-side Web Programs: Invited Talk

    Extending Database Technology (EDBT) / Database Theory (ICDT) Workshops 2010

  54. Small Specifications for Tree Update

    Web Services and Formal Methods (WS-FM) 2009

  55. A Process Model of Rho GTP-Binding Proteins

    • Luca Cardelli
    • Emmanuelle Caron
    • Philippa Gardner
    • Ozan Kahramanoğulları
    • Andrew Phillips

    Theoretical Computer Science 2009

  56. Decidability of Context Logic

  57. Footprints in Local Reasoning

    Logical Methods in Computer Science 2009

  58. Automatic Parallelization with Separation Logic

    ESOP 2009

  59. A Process Model of Actin Polymerisation

    • Luca Cardelli
    • Emmanuelle Caron
    • Philippa Gardner
    • Ozan Kahramanogullari
    • Andrew Phillips

    Electronic Notes in Theoretical Computer Science 2009

  60. Reasoning about High-Level Tree Update and its Low-Level Implementation

  61. Local Hoare Reasoning about DOM

    Principles of Database Systems (PODS) 2008

  62. Footprints in Local Reasoning

    Foundations of Software Science and Computation (FOSSACS) 2008

  63. Behavioural Equivalences for Dynamic Web Data

    Logic and Algebraic Programming 2008

  64. DOM: Towards a Formal Specification

    Programming Language Technologies for XML (PLAN-X) 2008

  65. A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis

    Electronic Notes in Theoretical Computer Science 2008

  66. Adjunct Elimination in Context Logic for Trees

    Asian Symposium on Programming Languages and Systems (ALPAS) 2007

  67. An Introduction to Context Logic

    Workshop on Logic, Language, Information and Computation (WoLLIC) 2007

  68. Manipulating Trees with Hidden Labels

    Electronic Notes in Theoretical Computer Science 2007

  69. Local Reasoning about Data Update

    Electronic Notes in Theoretical Computer Science 2007

  70. Linear Forwarders

    Information and Computation 2007

  71. Expressiveness and Complexity of Graph Logic

    Information and Computation 2007

  72. Context Logic as Modal Logic: Completeness and Parametric Inexpressivity

    POPL 2007

  73. Editorial

    Theoretical Computer Science 2006

  74. Local Reasoning About Tree Update

    Electronic Notes in Theoretical Computer Science 2006

  75. A Note on Context Logic

  76. Modelling Dynamic Web Data

    Theoretical Computer Science 2005

  77. Explicit Fusions

    Theoretical Computer Science 2005

  78. From Separation Logic to First-Order Logic

    Foundations of Software Science and Computation (FOSSACS) 2005

  79. Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems

    04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems

  80. Context Logic and Tree Update

    POPL 2005

  81. Adjunct Elimination Through Games in Static Ambient Logic

    Foundations of Software Technology and Theoretical Computer Science (FSTTCS) 2004

  82. Behavioural Equivalences for Dynamic Web Data

    Theoretical Compuer Science (TCS) 2004

  83. Strong Bisimulation for the Explicit Fusion Calculus

    Foundations of Software Science and Computation (FOSSACS) 2004

  84. Modelling Dynamic Web Data

    Database Programming Languages (DBPL) 2003

  85. Linear Forwarders

    Concurrency Theory (CONCUR) 2003

  86. Ubiquitous Data

  87. Manipulating Trees with Hidden Labels

    Foundations of Software Science and Computation (FOSSACS) 2003

  88. The Fusion Machine

    Concurrency Theory (CONCUR) 2002

  89. A Spatial Logic for Querying Graphs

    Automata, Languages and Programming (ICALP) 2002

  90. From Process Calculi to Process Frameworks

    Concurrency Theory (CONCUR) 2000

  91. Explicit Fusions

    Mathematical Foundations of Computer Science (MFCS) 2000

  92. Closed Action Calculi

    Theoretical Computer Science 1999

  93. Symmetric Action Calculi

  94. A Type-theoretic Description of Action Calculi

    Electronic Notes in Theoretical Computer Science 1997

  95. Types and Models for Higher-Order Action Calculi

    Theoretical Aspects of Computer Software (TACS) 1997

  96. From Action Calculi to Linear Logic

    Computer Science Logic (CSL) 1997

  97. Equivalences between Logics and Their Representing Type Theories

    Mathematical Structures in Computer Science 1995

  98. A Name-free Account of Action Calculi

    Electronic Notes in Theoretical Computer Science 1995

  99. Discovering Needed Reductions Using Type Theory

    Theoretical Aspects of Computer Software (TACS) 1994

  100. A New Type Theory for Representing Logics

    Logic Programming and Automated Reasoning (LPAR) 1993

  101. Representing Logics in Type Theory

    Ph.D. Thesis, University of Edinburgh, UK, 1992

  102. Unfold/Fold Transformations of Logic Programs

    Computational Logic - Essays in Honor of Alan Robinson, pp. 565–583