Publications

2017

  1. Towards Logic-based Verification of JavaScript Programs

    • José Fragoso Santos
    • Philippa Gardner
    • Petar Maksimović
    • Daiva Naudžiūnienė

    Aug 2017

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

  2. Abstract Specifications for Concurrent Maps

    • Shale Xiong
    • Pedro da Rocha Pinto
    • Gian Ntzik
    • Philippa Gardner

    Apr 2017

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

  3. Reasoning About POSIX File Systems

    • Gian Ntzik

    2017

    Ph.D. Thesis, Imperial College London

  4. Reasoning with Time and Data Abstractions

    • Pedro da Rocha Pinto

    2017

    Ph.D. Thesis, Imperial College London

  5. Abstraction, Refinement and Concurrent Reasoning

    • Azalea Raad

    2017

    Ph.D. Thesis, Imperial College London

2016

  1. Modular Termination Verification for Non-blocking Concurrency

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Philippa Gardner
    • Julian Sutherland

    Apr 2016

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

  2. Verifying Concurrent Graph Algorithms

    • Azalea Raad
    • Aquinas Hobor
    • Jules Villard
    • Philippa Gardner

    2016

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

  3. DOM: Specification and Client Reasoning

    • Azalea Raad
    • José Fragoso Santos
    • Philippa Gardner

    2016

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

2015

  1. Fault-tolerant Resource Reasoning

    • Gian Ntzik
    • Pedro da Rocha Pinto
    • Philippa Gardner

    Dec 2015

    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

    • Gian Ntzik
    • Philippa Gardner

    Oct 2015

    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)

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Philippa Gardner

    Jun 2015

    Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS’15), pp. 3–18

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

    • Philippa Gardner
    • Gareth Smith
    • Conrad Watt
    • Thomas Wood

    2015

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

  5. CoLoSL: Concurrent Local Subjective Logic

    • Azalea Raad
    • Jules Villard
    • Philippa Gardner

    2015

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

2014

  1. TaDA: A Logic for Time and Data Abstraction

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Philippa Gardner

    Jul 2014

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

  2. A Trusted Mechanised JavaScript Specification

    • Martin Bodin
    • Arthur Charguéraud
    • Daniele Filaretti
    • Philippa Gardner
    • Sergio Maffeis
    • Daiva Naudžiūnienė
    • Alan Schmitt
    • Gareth Smith

    2014

    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

    • Philippa Gardner
    • Gian Ntzik
    • Adam Wright

    2014

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

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

    • Philippa Gardner
    • Azalea Raad
    • Mark J. Wheelhouse
    • Adam Wright

    2014

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

2013

  1. Views: Compositional Reasoning for Concurrent Programs

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

    2013

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

2012

  1. Towards a Program Logic for JavaScript

    • Philippa Gardner
    • Sergio Maffeis
    • Gareth Smith

    2012

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

2011

  1. A Simple Abstraction for Complex Concurrent Indexes

    • Pedro da Rocha Pinto
    • Thomas Dinsdale-Young
    • Mike Dodds
    • Philippa Gardner
    • Mark J. Wheelhouse

    Oct 2011

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

  2. Abstract Local Reasoning for Program Modules

    • Thomas Dinsdale-Young
    • Philippa Gardner
    • Mark J. Wheelhouse

    2011

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

2010

  1. Adjunct elimination in Context Logic for Trees

    • Cristiano Calcagno
    • Thomas Dinsdale-Young
    • Philippa Gardner

    2010

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

  2. Concurrent Abstract Predicates

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

    2010

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

  3. Abstraction and Refinement for Local Reasoning

    • Thomas Dinsdale-Young
    • Philippa Gardner
    • Mark J. Wheelhouse

    2010

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

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

    • Philippa Gardner

    2010

    Proceedings of the 2010 EDBT/ICDT Workshops

2009

  1. Small Specifications for Tree Update

    • Philippa Gardner
    • Mark J. Wheelhouse

    2009

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

  2. Automatic Parallelization with Separation Logic

    • Mohammad Raza
    • Cristiano Calcagno
    • Philippa Gardner

    2009

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

  3. Footprints in Local Reasoning

    • Mohammad Raza
    • Philippa Gardner

    2009

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

2008

  1. DOM: Towards a Formal Specification

    • Philippa Gardner
    • Gareth Smith
    • Mark J. Wheelhouse
    • Uri Zarfaty

    2008

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

  2. Local Hoare Reasoning about DOM

    • Philippa Gardner
    • Gareth Smith
    • Mark J. Wheelhouse
    • Uri Zarfaty

    2008

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

  3. Behavioural Equivalences for Dynamic Web Data

    • Sergio Maffeis
    • Philippa Gardner

    2008

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

  4. Footprints in Local Reasoning

    • Mohammad Raza
    • Philippa Gardner

    2008

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

2007

  1. Adjunct Elimination in Context Logic for Trees

    • Cristiano Calcagno
    • Thomas Dinsdale-Young
    • Philippa Gardner

    2007

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

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

    • Cristiano Calcagno
    • Philippa Gardner
    • Uri Zarfaty

    2007

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

  3. Local Reasoning about Data Update

    • Cristiano Calcagno
    • Philippa Gardner
    • Uri Zarfaty

    2007

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

  4. Manipulating Trees with Hidden Labels

    • Luca Cardelli
    • Philippa Gardner
    • Giorgio Ghelli

    2007

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

  5. Expressiveness and Complexity of Graph Logic

    • Anuj Dawar
    • Philippa Gardner
    • Giorgio Ghelli

    2007

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

  6. An Introduction to Context Logic

    • Philippa Gardner
    • Uri Zarfaty

    2007

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

2005

  1. From Separation Logic to First-Order Logic

    • Cristiano Calcagno
    • Philippa Gardner
    • Matthew Hague

    2005

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

  2. Context Logic and Tree Update

    • Cristiano Calcagno
    • Philippa Gardner
    • Uri Zarfaty

    2005

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

  3. Modelling Dynamic Web Data

    • Philippa Gardner
    • Sergio Maffeis

    2005

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

2004

  1. Adjunct Elimination Through Games in Static Ambient Logic

    • Anuj Dawar
    • Philippa Gardner
    • Giorgio Ghelli

    2004

    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

    • Sergio Maffeis
    • Philippa Gardner

    2004

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

2003

  1. Manipulating Trees with Hidden Labels

    • Luca Cardelli
    • Philippa Gardner
    • Giorgio Ghelli

    2003

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

  2. Modelling Dynamic Web Data

    • Philippa Gardner
    • Sergio Maffeis

    2003

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

2002

  1. A Spatial Logic for Querying Graphs

    • Luca Cardelli
    • Philippa Gardner
    • Giorgio Ghelli

    2002

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