2024

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

2023

  1. Symbolic Debugging with Gillian

    Proceedings of the 1st ACM International Workshop on Future Debugging Techniques, pp. 1–2

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

    37th European Conference on Object-Oriented Programming (ECOOP 2023), pp. 19:1–19:27

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

    44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), pp. 151:1–151:25

2022

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

    Ph.D. Thesis, Imperial College London

  2. A Certified Algorithm for AC-Unification

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

    7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pp. 8:1–8:21

  3. Nominal Anti-Unification with Atom-Variables

    7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pp. 7:1–7:22

2021

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

    ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021., vol. 43(4)

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

    Proceedings of the 33rd Computer Aided Verification International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Part II, pp. 827–850

  3. Two Mechanisations of WebAssembly 1.0

    Proceedings of the 24th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021, pp. 61–79

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

    27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference), pp. 11:1–11:24

2020

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

    Proceedings of the 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), pp. 31:1–31:23

  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. Parametric Operational Semantics for Consistency Models

    Ph.D. Thesis, Imperial College London

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

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

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

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

2019

  1. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

    Proceedings of the 46th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’19), vol. 3( POPL)

  2. Skeletal Semantics and their Interpretations

    Proceedings of the 46th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’19)

  3. A Program Logic for First-Order Encapsulated WebAssembly

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

2018

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

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

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

  3. A Perspective on Specifying and Verifying Concurrent Modules

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

  4. A Concurrent Specification of POSIX File Systems

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

  5. JSExplain: a Double Debugger for JavaScript

    WWW ’18 Companion: The 2018 Web Conference Companion, April 23–27, 2018, Lyon, France

  6. JaVerT: JavaScript Verification Toolchain

    Proceedings of the 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’18), pp. 50:1–50:33

  7. An Infrastructure for Tractable Verification of JavaScript Programs

    Ph.D. Thesis, Imperial College London

2017

  1. Algebraic Laws for Weak Consistency

    Proceedings of 28th International Conference on Concurrency Theory, (Concur 2017)

  2. Verified Trustworthy Software Systems

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

  3. Towards Logic-based Verification of JavaScript Programs

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

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

    Proceedings of 30th IEEE Computer Security Foundations Symposium, (CSF 2017)

  5. Abstraction, Refinement and Concurrent Reasoning

    Ph.D. Thesis, Imperial College London

  6. Reasoning with Time and Data Abstractions

    Ph.D. Thesis, Imperial College London

  7. Caper: Automatic Verification for Fine-grained Concurrency

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

  8. Abstract Specifications for Concurrent Maps

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

  9. Reasoning About POSIX File Systems

    Ph.D. Thesis, Imperial College London

2016

  1. Modular Termination Verification for Non-blocking Concurrency

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

  2. DOM: Specification and Client Reasoning

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

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

    Journal of Computer Security, vol. 1(24), pp. 91–136

  4. Verifying Concurrent Graph Algorithms

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

2015

  1. Fault-tolerant Resource Reasoning

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

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

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

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

  4. CoLoSL: Concurrent Local Subjective Logic

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

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

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

  6. Modular Monitor Extensions for Information Flow Security in JavaScript

    Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers, pp. 47–62

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

    Trustworthy Global Computing - 10thh International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers, pp. 63–78

2014

  1. TaDA: A Logic for Time and Data Abstraction

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

  2. A Trusted Mechanised JavaScript Specification

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

  3. Local Reasoning for the POSIX File System

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

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

2013

  1. Structural Separation Logic

    • Adam Douglas Wright

    Ph.D. Thesis, Imperial College London

  2. JuS: Squeezing the Sense out of JavaScript Programs

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

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

  4. Programming Languages and Systems

    Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings

2012

  1. Segment Logic

    • Mark James Wheelhouse

    Ph.D. Thesis, Imperial College London

  2. Towards a Program Logic for JavaScript

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

  3. Processes in Space

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

2011

  1. Abstract Data and Local Reasoning

    • Thomas Dinsdale-Young

    Ph.D. Thesis, Imperial College London

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

  3. Local Reasoning about Web Programs

    • Gareth D. Smith

    Ph.D. Thesis, Imperial College London

  5. Abstract Local Reasoning for Program Modules

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

2010

  1. Resource Reasoning and Labelled Separation Logic

    • Mohammad Raza

    Imperial College London

  2. Resource Reasoning about Mashups

    VSTTE Theory Workshop 2010

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

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

  5. Adjunct elimination in Context Logic for Trees

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

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

  7. Abstraction and Refinement for Local Reasoning

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

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

    Proceedings of the 2010 EDBT/ICDT Workshops

2009

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

  2. Database Programming Languages

    Database Programming Languages - DBPL 2009, 12th International Symposium, Lyon, France, August 24, 2009. Proceedings

  3. Small Specifications for Tree Update

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

  4. Automatic Parallelization with Separation Logic

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

  5. Footprints in Local Reasoning

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

  6. Decidability of Context Logic

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

2008

  1. Behavioural Equivalences for Dynamic Web Data

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

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

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

  3. DOM: Towards a Formal Specification

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

  4. Local Hoare Reasoning about DOM

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

  5. Footprints in Local Reasoning

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

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

2007

  1. Adjunct Elimination in Context Logic for Trees

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

  2. Local Reasoning about Data Update

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

  3. Manipulating Trees with Hidden Labels

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

  4. Linear Forwarders

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

  5. Expressiveness and Complexity of Graph Logic

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

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

  7. An Introduction to Context Logic

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

  8. Context logic and Tree Update

    • Uri D Zarfaty

    Imperial College London

2006

  1. Local Reasoning About Tree Update

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

  2. Editorial

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

2005

  1. Modelling Dynamic Web Data

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

  2. A Note on Context Logic

  3. Explicit Fusions

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

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

  5. Context Logic and Tree Update

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

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

2004

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

  2. Behavioural Equivalences for Dynamic Web Data

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

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

  4. Preface CONCUR 2004, Proceedings

    CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings

2003

  1. Linear Forwarders

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

  2. Modelling Dynamic Web Data

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

  3. Ubiquitous Data

  4. Manipulating Trees with Hidden Labels

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

2002

  1. The Fusion Machine

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

  2. A Spatial Logic for Querying Graphs

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

2000

  1. Explicit Fusions

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

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

1999

  1. Symmetric Action Calculi

  2. Closed Action Calculi

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

1997

  1. A Type-theoretic Description of Action Calculi

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

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

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

1995

  1. A Name-free Account of Action Calculi

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

  2. Equivalences between Logics and Their Representing Type Theories

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

1994

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

1993

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

1992

  1. Representing Logics in Type Theory

    Ph.D. Thesis, University of Edinburgh, UK

1991

  1. Unfold/Fold Transformations of Logic Programs

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