Publications and PhD Theses

2026

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

2025

File Info
Designing and Maintaining an Efficient WebAssembly Mechanisation
- Xiaojia Rao
Ph.D. Thesis, Imperial College London, 2025
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
File Info
A Hybrid Approach to Semi-automated Rust Verification
- Sacha-Élie Ayoun
- Xavier Denis
- Petar Maksimović
- Philippa Gardner
PLDI 2025
File Info
Gillian: Foundations, Implementation, and Applications of Compositional Symbolic Execution
- Sacha-Élie Ayoun
Ph.D. Thesis, Imperial College London, 2025
Info
Progressful Interpreters for Efficient WebAssembly Mechanisation
- Xiaojia Rao
- Stefan Radziuk
- Conrad Watt
- Philippa Gardner
POPL 2025

2024

Info
Matching Plans for Frame Inference in Compositional Reasoning
- Andreas Lööw
- Daniele Nantes-Sobrinho
- Sacha-Élie Ayoun
- Petar Maksimović
- Philippa Gardner
ECOOP 2024
Info
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning
- Andreas Lööw
- Daniele Nantes-Sobrinho
- Sacha-Élie Ayoun
- Caroline Cronjäger
- Petar Maksimović
- Philippa Gardner
ECOOP 2024
File Info
Bringing the WebAssembly Standard up to Speed with SpecTec
- Dongjun Youn
- Wonho Shin
- Jaehyun Lee
- Sukyoung Ryu
- Joachim Breitner
- Philippa Gardner
- Sam Lindley
- Matija Pretnar
- Xiaojia Rao
- Conrad Watt
- Andreas Rossberg
PLDI 2024

2023

File Info
Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding
- Petar Maksimović
- Caroline Cronjäger
- Andreas Lööw
- Julian Sutherland
- Philippa Gardner
ECOOP 2023
File Info
Symbolic Debugging with Gillian
- Nat Karmios
- Sacha-Élie Ayoun
- Philippa Gardner
Future Debugging Techniques (DEBT) @ ECOOP 2023
File Info
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
- Xiaojia Rao
- Aïna Linn Georges
- Maxime Legoupil
- Conrad Watt
- Jean Pichon-Pharabod
- Philippa Gardner
- Lars Birkedal
PLDI 2023

2022

File Info
A Trusted Infrastructure for Symbolic Analysis of Event-based Web APIs
- Gabriela Sampaio
Ph.D. Thesis, Imperial College London, 2022

2021

File Info
Two Mechanisations of WebAssembly 1.0
- Conrad Watt
- Xiaojia Rao
- Jean Pichon-Pharabod
- Martin Bodin
- Philippa Gardner
Formal Methods (FM) 2021
File Info
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
- Emanuele D’Osualdo
- Azadeh Farzan
- Philippa Gardner
- Julian Sutherland
Transactions on Programming Languages and Systems (TOPLAS) 2021
File Info
Gillian, Part II: Real-World Verification for JavaScript and C
- Petar Maksimovic
- Sacha-Élie Ayoun
- José Fragoso Santos
- Philippa Gardner
CAV 2021

2020

File Info
Data Consistency in Transactional Storage Systems: a Centralised Approach
- Shale Xiong
- Andrea Cerone
- Azalea Raad
- Philippa Gardner
ECOOP 2020
File Info
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications
- Gabriela Sampaio
- José Fragoso Santos
- Petar Maksimovic
- Philippa Gardner
ECOOP 2020
File Info
Parametric Operational Semantics for Consistency Models
- Shale Xiong
Ph.D. Thesis, Imperial College London, 2020
File Info
Gillian, Part I: A Multi-language Platform for Symbolic Execution
- José Fragoso Santos
- Petar Maksimovic
- Sacha-Élie Ayoun
- Philippa Gardner
PLDI 2020

2019

File Info
A Program Logic for First-Order Encapsulated WebAssembly
- Conrad Watt
- Petar Maksimovic
- Neelakantan R. Krishnaswami
- Philippa Gardner
ECOOP 2019
File Info
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
- José Fragoso Santos
- Petar Maksimovic
- Gabriela Sampaio
- Philippa Gardner
POPL 2019
File Info
Skeletal Semantics and their Interpretations
- Martin Bodin
- Philippa Gardner
- Thomas Jensen
- Alan Schmitt
POPL 2019

2018

File Info
JaVerT: JavaScript Verification and Testing Framework: Invited Talk
- Philippa Gardner
Principles and Practice of Declarative Programming (PPDP) 2018
File Info
Symbolic Execution for JavaScript
- José Fragoso Santos
- Petar Maksimovic
- Théotime Grohens
- Julian Dolby
- Philippa Gardner
Principles and Practice of Declarative Programming (PPDP) 2018
File Info
JaVerT: JavaScript Verification Toolchain
- José Fragoso Santos
- Petar Maksimovic
- Daiva Naudziuniene
- Thomas Wood
- Philippa Gardner
POPL 2018
File Info
A Perspective on Specifying and Verifying Concurrent Modules
- Thomas Dinsdale-Young
- Pedro da Rocha Pinto
- Philippa Gardner
Journal of Logical and Algebraic Methods in Programming 2018
File Info
A Concurrent Specification of POSIX File Systems
- Gian Ntzik
- Pedro da Rocha Pinto
- Julian Sutherland
- Philippa Gardner
ECOOP 2018
File Info
An Infrastructure for Tractable Verification of JavaScript Programs
- Daiva Naudziuniene
Ph.D. Thesis, Imperial College London, 2018

2017

File Info
Verified Trustworthy Software Systems
- Philippa Gardner
Philosophical Transactions of the Royal Society of London A 2017
File Info
Towards Logic-based Verification of JavaScript Programs
- José Fragoso Santos
- Philippa Gardner
- Petar Maksimovic
- Daiva Naudziuniene
Conference on Automated Deduction (CADE) 2017
File Info
Abstraction, Refinement and Concurrent Reasoning
- Azalea Raad
Ph.D. Thesis, Imperial College London, 2017
File Info
Reasoning About POSIX File Systems
- Gian Ntzik
Ph.D. Thesis, Imperial College London, 2017
File Info
Reasoning with Time and Data Abstractions
- Pedro da Rocha Pinto
Ph.D. Thesis, Imperial College London, 2017
File Info
Abstract Specifications for Concurrent Maps
- Shale Xiong
- Pedro da Rocha Pinto
- Gian Ntzik
- Philippa Gardner
ESOP 2017

2016

File Info
Verifying Concurrent Graph Algorithms
- Azalea Raad
- Aquinas Hobor
- Jules Villard
- Philippa Gardner
Asian Symposium on Prograaming Languages and Systems (APLAS) 2016
File Info
DOM: Specification and Client Reasoning
- Azalea Raad
- José Fragoso Santos
- Philippa Gardner
Asian Symposium on Programming Languages and Systems (APLAS) 2016
File Info
Modular Termination Verification for Non-blocking Concurrency
- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Philippa Gardner
- Julian Sutherland
ESOP 2016

2015

File Info
Fault-tolerant Resource Reasoning
- Gian Ntzik
- Pedro da Rocha Pinto
- Philippa Gardner
Asian Symposium on Programming Languages and Systems (APLAS) 2015
File Info
Reasoning about the POSIX File System: Local Update and Global Pathnames
- Gian Ntzik
- Philippa Gardner
OOPSLA 2015
File Info
Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)
- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Philippa Gardner
Mathematical Foundations of Programming Semantics (MFPS) 2015
File Info
CoLoSL: Concurrent Local Subjective Logic
- Azalea Raad
- Jules Villard
- Philippa Gardner
ESOP 2015
File Info
A Trusted Mechanised Specification of JavaScript: One Year On
- Philippa Gardner
- Gareth Smith
- Conrad Watt
- Thomas Wood
CAV 2015

2014

File Info
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
- Philippa Gardner
- Azalea Raad
- Mark J. Wheelhouse
- Adam Wright
Mathematical Foundations of Programming Semantics (MFPS) 2014
File Info
TaDA: A Logic for Time and Data Abstraction
- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Philippa Gardner
ECOOP 2014
File Info
Local Reasoning for the POSIX File System
- Philippa Gardner
- Gian Ntzik
- Adam Wright
ESOP 2014
File Info
A Trusted Mechanised JavaScript Specification
- Martin Bodin
- Arthur Charguéraud
- Daniele Filaretti
- Philippa Gardner
- Sergio Maffeis
- Daiva Naudziuniene
- Alan Schmitt
- Gareth Smith
POPL 2014

2013

File Info
Structural Separation Logic
- Adam Douglas Wright
Ph.D. Thesis, Imperial College London, 2013
File Info
JuS: Squeezing the Sense out of JavaScript Programs
- Philipa Gardner
- Daiva Naudziuniene
- Gareth Smith
Tools for JavaScript Analysis (JSTools) @ ECOOP 2013
File Info
Views: Compositional Reasoning for Concurrent Programs
- Thomas Dinsdale-Young
- Lars Birkedal
- Philippa Gardner
- Matthew J. Parkinson
- Hongseok Yang
POPL 2013

2012

File Info
Segment Logic
- Mark James Wheelhouse
Ph.D. Thesis, Imperial College London, 2012
Info
Processes in Space
- Luca Cardelli
- Philippa Gardner
Theoretical Computer Science 2012
File Info
Towards a Program Logic for JavaScript
- Philippa Gardner
- Sergio Maffeis
- Gareth Smith
POPL 2012

2011

File Info
Abstract Data and Local Reasoning
- Thomas Dinsdale-Young
Ph.D. Thesis, Imperial College London, 2011
File Info
A Simple Abstraction for Complex Concurrent Indexes
- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Mike Dodds
- Philippa Gardner
- Mark J. Wheelhouse
OOPSLA 2011
File Info
Abstract Local Reasoning for Program Modules
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark J. Wheelhouse
Algebra and Coalgebra in Computer Science (CALCO) 2011
File Info
Local Reasoning about Web Programs
- Gareth D. Smith
Ph.D. Thesis, Imperial College London, 2011

2010

File Info
Resource Reasoning and Labelled Separation Logic
- Mohammad Raza
Ph.D. Thesis, Imperial College London, 2010
Info
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
File Info
Resource Reasoning about Mashups
- Philippa A Gardner
- Gareth D Smith
- Adam D Wright
Verified Software: Theories, Tools and Experiments (VSTTE) 2010
Info
Locality Refinement
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark Wheelhouse
Verified Software: Theories, Tools and Experiments (VSTTE) 2010
File Info
Abstraction and Refinement for Local Reasoning
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark J. Wheelhouse
Verified Software: Theories, Tools and Experiments (VSTTE) 2010
File Info
Concurrent Abstract Predicates
- Thomas Dinsdale-Young
- Mike Dodds
- Philippa Gardner
- Matthew J. Parkinson
- Viktor Vafeiadis
ECOOP 2010
Info
Processes in Space
- Luca Cardelli
- Philippa Gardner
Programs, Proofs, Processes @ Computability in Europe (CiE) 2010
File Info
Adjunct Elimination in Context Logic for Trees
- Cristiano Calcagno
- Thomas Dinsdale-Young
- Philippa Gardner
Information and Computation 2010
File Info
Reasoning About Client-side Web Programs: Invited Talk
- Philippa Gardner
Extending Database Technology (EDBT) / Database Theory (ICDT) Workshops 2010

2009

File Info
Small Specifications for Tree Update
- Philippa Gardner
- Mark J. Wheelhouse
Web Services and Formal Methods (WS-FM) 2009
File Info
A Process Model of Rho GTP-Binding Proteins
- Luca Cardelli
- Emmanuelle Caron
- Philippa Gardner
- Ozan Kahramanoğulları
- Andrew Phillips
Theoretical Computer Science 2009
File Info
Decidability of Context Logic
- Christiano Calcagno
- Thomas Dinsdale-Young
- Philippa Gardner
File Info
Footprints in Local Reasoning
- Mohammad Raza
- Philippa Gardner
Logical Methods in Computer Science 2009
File Info
Automatic Parallelization with Separation Logic
- Mohammad Raza
- Cristiano Calcagno
- Philippa Gardner
ESOP 2009
Info
A Process Model of Actin Polymerisation
- Luca Cardelli
- Emmanuelle Caron
- Philippa Gardner
- Ozan Kahramanogullari
- Andrew Phillips
Electronic Notes in Theoretical Computer Science 2009
File Info
Reasoning about High-Level Tree Update and its Low-Level Implementation
- Philippa Gardner
- Uri Zarfaty

2008

File Info
Local Hoare Reasoning about DOM
- Philippa Gardner
- Gareth Smith
- Mark J. Wheelhouse
- Uri Zarfaty
Principles of Database Systems (PODS) 2008
Info
Footprints in Local Reasoning
- Mohammad Raza
- Philippa Gardner
Foundations of Software Science and Computation (FOSSACS) 2008
File Info
Behavioural Equivalences for Dynamic Web Data
- Sergio Maffeis
- Philippa Gardner
Logic and Algebraic Programming 2008
File Info
DOM: Towards a Formal Specification
- Philippa Gardner
- Gareth Smith
- Mark J. Wheelhouse
- Uri Zarfaty
Programming Language Technologies for XML (PLAN-X) 2008
Info
A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis
- Luca Cardelli
- Philippa Gardner
- Ozan Kahramanogullari
Electronic Notes in Theoretical Computer Science 2008

2007

File Info
Adjunct Elimination in Context Logic for Trees
- Cristiano Calcagno
- Thomas Dinsdale-Young
- Philippa Gardner
Asian Symposium on Programming Languages and Systems (ALPAS) 2007
Info
An Introduction to Context Logic
- Philippa Gardner
- Uri Zarfaty
Workshop on Logic, Language, Information and Computation (WoLLIC) 2007
File Info
Manipulating Trees with Hidden Labels
- Luca Cardelli
- Philippa Gardner
- Giorgio Ghelli
Electronic Notes in Theoretical Computer Science 2007
File Info
Local Reasoning about Data Update
- Cristiano Calcagno
- Philippa Gardner
- Uri Zarfaty
Electronic Notes in Theoretical Computer Science 2007
File Info
Linear Forwarders
- Philippa Gardner
- Cosimo Laneve
- Lucian Wischik
Information and Computation 2007
File Info
Expressiveness and Complexity of Graph Logic
- Anuj Dawar
- Philippa Gardner
- Giorgio Ghelli
Information and Computation 2007
File Info
Context Logic as Modal Logic: Completeness and Parametric Inexpressivity
- Cristiano Calcagno
- Philippa Gardner
- Uri Zarfaty
POPL 2007
File Info
Context logic and Tree Update
- Uri D Zarfaty
Ph.D. Thesis, Imperial College London, 2007

2006

Info
Editorial
- Philippa Gardner
- Nobuko Yoshida
Theoretical Computer Science 2006
File Info
Local Reasoning About Tree Update
- Uri Zarfaty
- Philippa Gardner
Electronic Notes in Theoretical Computer Science 2006

2005

File Info
A Note on Context Logic
- Philippa Gardner
File Info
Modelling Dynamic Web Data
- Philippa Gardner
- Sergio Maffeis
Theoretical Computer Science 2005
File Info
Explicit Fusions
- Lucian Wischik
- Philippa Gardner
Theoretical Computer Science 2005
File Info
From Separation Logic to First-Order Logic
- Cristiano Calcagno
- Philippa Gardner
- Matthew Hague
Foundations of Software Science and Computation (FOSSACS) 2005
File Info
Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems
- Barbara König
- Ugo Montanari
- Philippa Gardner
04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems
File Info
Context Logic and Tree Update
- Cristiano Calcagno
- Philippa Gardner
- Uri Zarfaty
POPL 2005

2004

File Info
Adjunct Elimination Through Games in Static Ambient Logic
- Anuj Dawar
- Philippa Gardner
- Giorgio Ghelli
Foundations of Software Technology and Theoretical Computer Science (FSTTCS) 2004
File Info
Behavioural Equivalences for Dynamic Web Data
- Sergio Maffeis
- Philippa Gardner
Theoretical Compuer Science (TCS) 2004
File Info
Strong Bisimulation for the Explicit Fusion Calculus
- Lucian Wischik
- Philippa Gardner
Foundations of Software Science and Computation (FOSSACS) 2004

2003

File Info
Modelling Dynamic Web Data
- Philippa Gardner
- Sergio Maffeis
Database Programming Languages (DBPL) 2003
Info
Linear Forwarders
- Philippa Gardner
- Cosimo Laneve
- Lucian Wischik
Concurrency Theory (CONCUR) 2003
File Info
Ubiquitous Data
- Gavin Bierman
- Peter Buneman
- Philipa Gardner
File Info
Manipulating Trees with Hidden Labels
- Luca Cardelli
- Philippa Gardner
- Giorgio Ghelli
Foundations of Software Science and Computation (FOSSACS) 2003

2002

File Info
The Fusion Machine
- Philippa Gardner
- Cosimo Laneve
- Lucian Wischik
Concurrency Theory (CONCUR) 2002
File Info
A Spatial Logic for Querying Graphs
- Luca Cardelli
- Philippa Gardner
- Giorgio Ghelli
Automata, Languages and Programming (ICALP) 2002

2000

File Info
From Process Calculi to Process Frameworks
- Philippa Gardner
Concurrency Theory (CONCUR) 2000
File Info
Explicit Fusions
- Philippa Gardner
- Lucian Wischik
Mathematical Foundations of Computer Science (MFCS) 2000

1999

File Info
Closed Action Calculi
- Philippa Gardner
Theoretical Computer Science 1999
File Info
Symmetric Action Calculi
- Philippa Gardner
- Lucian J. Wischik

1997

File Info
A Type-theoretic Description of Action Calculi
- Philippa Gardner
Electronic Notes in Theoretical Computer Science 1997
Info
Types and Models for Higher-Order Action Calculi
- Philippa Gardner
- Masahito Hasegawa
Theoretical Aspects of Computer Software (TACS) 1997
File Info
From Action Calculi to Linear Logic
- Andrew G. Barber
- Philippa Gardner
- Masahito Hasegawa
- Gordon D. Plotkin
Computer Science Logic (CSL) 1997

1995

File Info
Equivalences between Logics and Their Representing Type Theories
- Philippa Gardner
Mathematical Structures in Computer Science 1995
File Info
A Name-free Account of Action Calculi
- Philippa Gardner
Electronic Notes in Theoretical Computer Science 1995

1994

File Info
Discovering Needed Reductions Using Type Theory
- Philippa Gardner
Theoretical Aspects of Computer Software (TACS) 1994

1993

Info
A New Type Theory for Representing Logics
- Philippa Gardner
Logic Programming and Automated Reasoning (LPAR) 1993

1992

File Info
Representing Logics in Type Theory
- Philippa Gardner
Ph.D. Thesis, University of Edinburgh, UK, 1992

1991

Info
Unfold/Fold Transformations of Logic Programs
- Philippa Gardner
- John C. Shepherdson
Computational Logic - Essays in Honor of Alan Robinson, pp. 565–583