2026

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

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

2025

  1. Designing and Maintaining an Efficient WebAssembly Mechanisation

    Ph.D. Thesis, Imperial College London, 2025

  2. Compositional Symbolic Execution for the Next 700 Memory Models

    OOPSLA 2025

  3. A Hybrid Approach to Semi-automated Rust Verification

    PLDI 2025

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

    Ph.D. Thesis, Imperial College London, 2025

  5. Progressful Interpreters for Efficient WebAssembly Mechanisation

    POPL 2025

2024

  1. Matching Plans for Frame Inference in Compositional Reasoning

    ECOOP 2024

  2. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

    ECOOP 2024

  3. Bringing the WebAssembly Standard up to Speed with SpecTec

    PLDI 2024

2023

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

    ECOOP 2023

  2. Symbolic Debugging with Gillian

    Future Debugging Techniques (DEBT) @ ECOOP 2023

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

    PLDI 2023

2022

  1. A Certified Algorithm for AC-Unification

    • Mauricio Ayala-Rincón
    • Maribel Fernández
    • Gabriel Ferreira Silva
    • Daniele Nantes

    Formal Structures for Computation and Deduction (FSCD) 2022

  2. Nominal Anti-Unification with Atom-Variables

    Formal Structures for Computation and Deduction (FSCD) 2022

  3. A Trusted Infrastructure for Symbolic Analysis of Event-based Web APIs

    Ph.D. Thesis, Imperial College London, 2022

2021

  1. Two Mechanisations of WebAssembly 1.0

    Formal Methods (FM) 2021

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

    Transactions on Programming Languages and Systems (TOPLAS) 2021

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

    CAV 2021

  4. Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes

    Types for Proofs and Programs (TYPES) 2021

2020

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

    ECOOP 2020

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

    ECOOP 2020

  3. Parametric Operational Semantics for Consistency Models

    Ph.D. Thesis, Imperial College London, 2020

  4. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

    Concurrency Theory (CONCUR) 2020

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

    PLDI 2020

2019

  1. A Program Logic for First-Order Encapsulated WebAssembly

    ECOOP 2019

  2. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

    POPL 2019

  3. Skeletal Semantics and their Interpretations

    POPL 2019

2018

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

    Principles and Practice of Declarative Programming (PPDP) 2018

  2. Symbolic Execution for JavaScript

    Principles and Practice of Declarative Programming (PPDP) 2018

  3. JaVerT: JavaScript Verification Toolchain

    POPL 2018

  4. A Perspective on Specifying and Verifying Concurrent Modules

    Journal of Logical and Algebraic Methods in Programming 2018

  5. A Concurrent Specification of POSIX File Systems

    ECOOP 2018

  6. An Infrastructure for Tractable Verification of JavaScript Programs

    Ph.D. Thesis, Imperial College London, 2018

  7. JSExplain: a Double Debugger for JavaScript

    Companion Proceedings of The Web Conference (WWW) 2018

2017

  1. Verified Trustworthy Software Systems

    Philosophical Transactions of the Royal Society of London A 2017

  2. Algebraic Laws for Weak Consistency

    Concurrency Theory (CONCUR) 2017

  3. Towards Logic-based Verification of JavaScript Programs

    Conference on Automated Deduction (CADE) 2017

  4. Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes

    Computer Security Foundations Symposium (CSF) 2017

  5. Abstraction, Refinement and Concurrent Reasoning

    Ph.D. Thesis, Imperial College London, 2017

  6. Reasoning About POSIX File Systems

    Ph.D. Thesis, Imperial College London, 2017

  7. Reasoning with Time and Data Abstractions

    Ph.D. Thesis, Imperial College London, 2017

  8. Abstract Specifications for Concurrent Maps

    ESOP 2017

  9. Caper: Automatic Verification for Fine-grained Concurrency

    ESOP 2017

2016

  1. Verifying Concurrent Graph Algorithms

    Asian Symposium on Prograaming Languages and Systems (APLAS) 2016

  2. DOM: Specification and Client Reasoning

    Asian Symposium on Programming Languages and Systems (APLAS) 2016

  3. Modular Termination Verification for Non-blocking Concurrency

    ESOP 2016

  4. Mashic Compiler: Mashup Sandboxing based on Inter-frame Communication

    Journal of Computer Security 2016

2015

  1. Fault-tolerant Resource Reasoning

    Asian Symposium on Programming Languages and Systems (APLAS) 2015

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

    OOPSLA 2015

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

    Mathematical Foundations of Programming Semantics (MFPS) 2015

  4. CoLoSL: Concurrent Local Subjective Logic

    ESOP 2015

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

    CAV 2015

  6. Modular Monitor Extensions for Information Flow Security in JavaScript

    Trustworthy Global Computing (TGC) 2015

  7. Hybrid Typing of Secure Information Flow in a JavaScript-Like Language

    Trustworthy Global Computing (TGC) 2015

2014

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

    Mathematical Foundations of Programming Semantics (MFPS) 2014

  2. TaDA: A Logic for Time and Data Abstraction

    ECOOP 2014

  3. Local Reasoning for the POSIX File System

    ESOP 2014

  4. A Trusted Mechanised JavaScript Specification

    POPL 2014

2013

  1. Structural Separation Logic

    • Adam Douglas Wright

    Ph.D. Thesis, Imperial College London, 2013

  2. JuS: Squeezing the Sense out of JavaScript Programs

    Tools for JavaScript Analysis (JSTools) @ ECOOP 2013

  3. Programming Languages and Systems

    ESOP 2013

  4. Views: Compositional Reasoning for Concurrent Programs

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

    POPL 2013

2012

  1. Segment Logic

    • Mark James Wheelhouse

    Ph.D. Thesis, Imperial College London, 2012

  2. Processes in Space

    Theoretical Computer Science 2012

  3. Towards a Program Logic for JavaScript

    POPL 2012

2011

  1. Abstract Data and Local Reasoning

    • Thomas Dinsdale-Young

    Ph.D. Thesis, Imperial College London, 2011

  2. A Simple Abstraction for Complex Concurrent Indexes

    OOPSLA 2011

  3. Abstract Local Reasoning for Program Modules

    Algebra and Coalgebra in Computer Science (CALCO) 2011

  4. Local Reasoning about Web Programs

    • Gareth D. Smith

    Ph.D. Thesis, Imperial College London, 2011

2010

  1. Resource Reasoning and Labelled Separation Logic

    • Mohammad Raza

    Ph.D. Thesis, Imperial College London, 2010

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

  3. Resource Reasoning about Mashups

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

  4. Locality Refinement

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

  5. Abstraction and Refinement for Local Reasoning

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

  6. Concurrent Abstract Predicates

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

    ECOOP 2010

  7. Processes in Space

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

  8. Adjunct Elimination in Context Logic for Trees

    Information and Computation 2010

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

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

2009

  1. Small Specifications for Tree Update

    Web Services and Formal Methods (WS-FM) 2009

  2. Database Programming Languages

    Database Programming Languages (DBPL) 2009

  3. A Process Model of Rho GTP-Binding Proteins

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

    Theoretical Computer Science 2009

  4. Decidability of Context Logic

  5. Footprints in Local Reasoning

    Logical Methods in Computer Science 2009

  6. Automatic Parallelization with Separation Logic

    ESOP 2009

  7. A Process Model of Actin Polymerisation

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

    Electronic Notes in Theoretical Computer Science 2009

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

2008

  1. Local Hoare Reasoning about DOM

    Principles of Database Systems (PODS) 2008

  2. Footprints in Local Reasoning

    Foundations of Software Science and Computation (FOSSACS) 2008

  3. Behavioural Equivalences for Dynamic Web Data

    Logic and Algebraic Programming 2008

  4. DOM: Towards a Formal Specification

    Programming Language Technologies for XML (PLAN-X) 2008

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

    Electronic Notes in Theoretical Computer Science 2008

2007

  1. Adjunct Elimination in Context Logic for Trees

    Asian Symposium on Programming Languages and Systems (ALPAS) 2007

  2. An Introduction to Context Logic

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

  3. Manipulating Trees with Hidden Labels

    Electronic Notes in Theoretical Computer Science 2007

  4. Local Reasoning about Data Update

    Electronic Notes in Theoretical Computer Science 2007

  5. Linear Forwarders

    Information and Computation 2007

  6. Expressiveness and Complexity of Graph Logic

    Information and Computation 2007

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

    POPL 2007

  8. Context logic and Tree Update

    • Uri D Zarfaty

    Ph.D. Thesis, Imperial College London, 2007

2006

  1. Editorial

    Theoretical Computer Science 2006

  2. Local Reasoning About Tree Update

    Electronic Notes in Theoretical Computer Science 2006

2005

  1. A Note on Context Logic

  2. Modelling Dynamic Web Data

    Theoretical Computer Science 2005

  3. Explicit Fusions

    Theoretical Computer Science 2005

  4. From Separation Logic to First-Order Logic

    Foundations of Software Science and Computation (FOSSACS) 2005

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

  6. Context Logic and Tree Update

    POPL 2005

2004

  1. Adjunct Elimination Through Games in Static Ambient Logic

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

  2. Preface CONCUR 2004, Proceedings

    Concurrency Theory (CONCUR) 2004

  3. Behavioural Equivalences for Dynamic Web Data

    Theoretical Compuer Science (TCS) 2004

  4. Strong Bisimulation for the Explicit Fusion Calculus

    Foundations of Software Science and Computation (FOSSACS) 2004

2003

  1. Modelling Dynamic Web Data

    Database Programming Languages (DBPL) 2003

  2. Linear Forwarders

    Concurrency Theory (CONCUR) 2003

  3. Ubiquitous Data

  4. Manipulating Trees with Hidden Labels

    Foundations of Software Science and Computation (FOSSACS) 2003

2002

  1. The Fusion Machine

    Concurrency Theory (CONCUR) 2002

  2. A Spatial Logic for Querying Graphs

    Automata, Languages and Programming (ICALP) 2002

2000

  1. From Process Calculi to Process Frameworks

    Concurrency Theory (CONCUR) 2000

  2. Explicit Fusions

    Mathematical Foundations of Computer Science (MFCS) 2000

1999

  1. Closed Action Calculi

    Theoretical Computer Science 1999

  2. Symmetric Action Calculi

1997

  1. A Type-theoretic Description of Action Calculi

    Electronic Notes in Theoretical Computer Science 1997

  2. Types and Models for Higher-Order Action Calculi

    Theoretical Aspects of Computer Software (TACS) 1997

  3. From Action Calculi to Linear Logic

    Computer Science Logic (CSL) 1997

1995

  1. Equivalences between Logics and Their Representing Type Theories

    Mathematical Structures in Computer Science 1995

  2. A Name-free Account of Action Calculi

    Electronic Notes in Theoretical Computer Science 1995

1994

  1. Discovering Needed Reductions Using Type Theory

    Theoretical Aspects of Computer Software (TACS) 1994

1993

  1. A New Type Theory for Representing Logics

    Logic Programming and Automated Reasoning (LPAR) 1993

1992

  1. Representing Logics in Type Theory

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

1991

  1. Unfold/Fold Transformations of Logic Programs

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