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’, 2021. In 2020 she was elected a Fellow of the Royal Academy of Engineering.

Group Publications

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

    33rd International Conference on Computer-Aided Verification, (CAV 2021)

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

    Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’20), June 15–20, 2020, London, UK

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

    34th European Conference on Object-Oriented Programming (ECOOP 2020)

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

    34th European Conference on Object-Oriented Programming (ECOOP 2020)

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

  6. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

    PACMPL, vol. 3( POPL)

  7. Skeletal Semantics and their Interpretations

    PACMPL, vol. 3( POPL)

  8. A Program Logic for First-Order Encapsulated WebAssembly

    33rd European Conference on Object-Oriented Programming (ECOOP 2019), pp. 9:1–9:30

  9. Symbolic Execution for JavaScript

    Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 11:1–11:14

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

    Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 1:1–1:4

  11. A Perspective on Specifying and Verifying Concurrent Modules

    Journal of Logical and Algebraic Methods in Programming, vol. 98, pp. 1–25

  12. A Concurrent Specification of POSIX File Systems

    32nd European Conference on Object-Oriented Programming (ECOOP 2018).

  13. JaVerT: JavaScript Verification Toolchain

    PACMPL, vol. 2(POPL), pp. 50:1–50:33

  14. Verified Trustworthy Software Systems

    Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, vol. 375(2104)

  15. Towards Logic-based Verification of JavaScript Programs

    Proceedings of 26th Conference on Automated Deduction (CADE 26)

  16. Abstract Specifications for Concurrent Maps

    Proceedings of the 26th European Symposium on Programming (ESOP’17), pp. 964–990

  17. Modular Termination Verification for Non-blocking Concurrency

    Proceedings of the 25th European Symposium on Programming (ESOP’16), pp. 176–201

  18. DOM: Specification and Client Reasoning

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 401–422

  19. Verifying Concurrent Graph Algorithms

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 314–334

  20. Fault-tolerant Resource Reasoning

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’15), pp. 169–188

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

    Proceedings of the 30th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’15), pp. 201–220

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

    Electr. Notes Theor. Comput. Sci., vol. 319, pp. 3–18

  23. CoLoSL: Concurrent Local Subjective Logic

    Proceedings of the 24th European Symposium on Programming (ESOP’15), pp. 710–735

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

    Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15), pp. 3–10

  25. TaDA: A Logic for Time and Data Abstraction

    Proceedings of the 28th European Conference on Object-Oriented Programming (ECOOP’14), pp. 207–231

  26. A Trusted Mechanised JavaScript Specification

    Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), pp. 87–100

  27. Local Reasoning for the POSIX File System

    Proceedings of the 23rd European Symposium on Programming (ESOP’14), pp. 169–188

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

    Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS’14), vol. 308, pp. 147–166

  29. JuS: Squeezing the Sense out of JavaScript Programs

    2nd Annual Workshop on Tools for JavaScript Analysis (JSTools ’13)

  30. Views: Compositional Reasoning for Concurrent Programs

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

    Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13), pp. 287–300

  31. Towards a Program Logic for JavaScript

    Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12), pp. 31–44

  32. Processes in Space

    Theor. Comput. Sci., vol. 431, pp. 40–55

  33. A Simple Abstraction for Complex Concurrent Indexes

    Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’11), pp. 845–864

  34. Abstract Local Reasoning for Program Modules

    Proceedings of the 4th International Conference on Algebra and Coalgebra in Computer Science (CALCO’11), pp. 36–39

  35. Resource Reasoning about Mashups

    VSTTE Theory Workshop 2010

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

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

    SIGMOD Record, vol. 39(1), pp. 54–57

  37. Processes in Space

    Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 - July 4, 2010. Proceedings, pp. 78–87

  38. Adjunct elimination in Context Logic for Trees

    Information and Computation, vol. 208(5), pp. 474–499

  39. Concurrent Abstract Predicates

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

    Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP’10), pp. 504–528

  40. Abstraction and Refinement for Local Reasoning

    Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE’10), pp. 199–215

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

    Proceedings of the 2010 EDBT/ICDT Workshops

  42. A Process Model of Actin Polymerisation

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

    Electr. Notes Theor. Comput. Sci., vol. 229(1), pp. 127–144

  43. Small Specifications for Tree Update

    Proceedings of the 6th International Workshop on Web Services and Formal Methods (WS-FM’09), pp. 178–195

  44. Automatic Parallelization with Separation Logic

    Proceedings of the 18th European Symposium on Programming (ESOP’09), pp. 348–362

  45. Footprints in Local Reasoning

    Logical Methods in Computer Science, vol. 5(2)

  46. Decidability of Context Logic

  47. A process model of Rho GTP-binding proteins

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

    Theoretical Computer Science, vol. 410(33), pp. 3166–3185

  48. Behavioural Equivalences for Dynamic Web Data

    Logic and Algebraic Programming, vol. 75(1), pp. 86–138

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

    Electr. Notes Theor. Comput. Sci., vol. 194(3), pp. 87–102

  50. DOM: Towards a Formal Specification

    Proceedings of the ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X’08)

  51. Local Hoare Reasoning about DOM

    Proceedings of the 27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS’08), pp. 261–270

  52. Footprints in Local Reasoning

    Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’08), pp. 201–215

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

  54. Adjunct Elimination in Context Logic for Trees

    Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS’07), pp. 255–270

  55. Local Reasoning about Data Update

    Electronic Notes on Theoretical Computer Science, vol. 172, pp. 133–175

  56. Manipulating Trees with Hidden Labels

    Electronic Notes in Theoretical Computer Science, vol. 172, pp. 177–201

  57. Linear Forwarders

    Inf. Comput., vol. 205(10), pp. 1526–1550

  58. Expressiveness and Complexity of Graph Logic

    Information and Computation, vol. 205(3), pp. 263–310

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

    Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’07), pp. 123–134

  60. An Introduction to Context Logic

    Proceedings of the 14th International Workshop on Logic, Language, Information and Computation (WoLLIC’07), pp. 189–202

  61. Local Reasoning About Tree Update

    Electr. Notes Theor. Comput. Sci., vol. 158, pp. 399–424

  62. Editorial

    Theor. Comput. Sci., vol. 358(2-3), pp. 149

  63. Modelling Dynamic Web Data

    Theoretical Computer Science, vol. 342(1), pp. 104–131

  64. A Note on Context Logic

  65. Explicit Fusions

    Theor. Comput. Sci., vol. 340(3), pp. 606–630

  66. From Separation Logic to First-Order Logic

    Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’05), pp. 395–409

  67. Context Logic and Tree Update

    Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05), pp. 271–282

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

  69. Adjunct Elimination Through Games in Static Ambient Logic

    Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’04), pp. 211–223

  70. Behavioural Equivalences for Dynamic Web Data

    Proceedings of 3rd International Conference on Theoretical Computer Science (TCS’04), pp. 535–548

  71. Strong Bisimulation for the Explicit Fusion Calculus

    Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, pp. 484–498

  72. Linear Forwarders

    CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings, pp. 408–422

  73. Modelling Dynamic Web Data

    Proceedings of 9th International Workshop on Database Programming Languages (DBPL’03), pp. 130–146

  74. Ubiquitous Data

  75. Manipulating Trees with Hidden Labels

    Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’03), pp. 216–232

  76. The Fusion Machine

    CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, pp. 418–433

  77. A Spatial Logic for Querying Graphs

    Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP’02), pp. 597–610

  78. Explicit Fusions

    Mathematical Foundations of Computer Science 2000, 25th International Symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings, pp. 373–382

  79. From Process Calculi to Process Frameworks

    CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, pp. 69–88

  80. Symmetric Action Calculi

  81. Closed Action Calculi

    Theor. Comput. Sci., vol. 228(1-2), pp. 77–103

  82. A Type-theoretic Description of Action Calculi

    Electr. Notes Theor. Comput. Sci., vol. 10, pp. 52

  83. From Action Calculi to Linear Logic

    Computer Science Logic, 11th International Workshop, CSL ’97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers, pp. 78–97

  84. Types and Models for Higher-Order Action Calculi

    Theoretical Aspects of Computer Software, Third International Symposium, TACS ’97, Sendai, Japan, September 23-26, 1997, Proceedings, pp. 583–603

  85. A Name-free Account of Action Calculi

    Electr. Notes Theor. Comput. Sci., vol. 1, pp. 214–231

  86. Equivalences between Logics and Their Representing Type Theories

    Mathematical Structures in Computer Science, vol. 5(3), pp. 323–349

  87. Discovering Needed Reductions Using Type Theory

    Theoretical Aspects of Computer Software, International Conference TACS ’94, Sendai, Japan, April 19-22, 1994, Proceedings, pp. 555–574

  88. A New Type Theory for Representing Logics

    Logic Programming and Automated Reasoning, 4th International Conference, LPAR’93, St. Petersburg, Russia, July 13–20, 1993 Proceedings, pp. 146–157

  89. Representing Logics in Type Theory

    Ph.D. Thesis, University of Edinburgh, UK

  90. Unfold/Fold Transformations of Logic Programs

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