Philippa Gardner

113 papers A* 8A 18B 22C 4Journal 38Unranked 20
YearRankTypeTitle / Venue / Authors
2026 J jnl
Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees, Extended Version.
CoRR
Nat Karmios, Sacha-Élie Ayoun, Philippa Gardner
2026 — conf
Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees.
TACAS (2)
Nat Karmios, Sacha-Élie Ayoun, Philippa Gardner
2025 J jnl
A Hybrid Approach to Semi-automated Rust Verification.
Proc. ACM Program. Lang.
Sacha-Élie Ayoun, Xavier Denis, Petar Maksimovic, Philippa Gardner
2025 J jnl
Compositional Symbolic Execution for the Next 700 Memory Models (Extended Version).
CoRR
Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Opale Sjöstedt, Philippa Gardner
2025 J jnl
Compositional Symbolic Execution for the Next 700 Memory Models.
Proc. ACM Program. Lang.
Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Opale Sjöstedt, Philippa Gardner
2025 J jnl
Progressful Interpreters for Efficient WebAssembly Mechanisation.
Proc. ACM Program. Lang.
Xiaojia Rao, Stefan Radziuk, Conrad Watt, Philippa Gardner
2024 J jnl
A hybrid approach to semi-automated Rust verification.
CoRR
Sacha-Élie Ayoun, Xavier Denis, Petar Maksimovic, Philippa Gardner
2024 J jnl
Bringing the WebAssembly Standard up to Speed with SpecTec.
Proc. ACM Program. Lang.
Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, Andreas Rossberg
2024 J jnl
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact).
Dagstuhl Artifacts Ser.
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimovic, Philippa Gardner
2024 J jnl
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version).
CoRR
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimovic, Philippa Gardner
2024 A conf
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning.
ECOOP
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimovic, Philippa Gardner
2024 A conf
Matching Plans for Frame Inference in Compositional Reasoning.
ECOOP
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimovic, Philippa Gardner
2023 A conf
Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding.
ECOOP
Petar Maksimovic, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, Philippa Gardner
2023 J jnl
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs.
Proc. ACM Program. Lang.
Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal
2023 — conf
Symbolic Debugging with Gillian.
DEBT@ISSTA
Nat Karmios, Sacha-Élie Ayoun, Philippa Gardner
2023 J jnl
Wasm SpecTec: Engineering a Formal Language Standard.
CoRR
Joachim Breitner, Philippa Gardner, Jaehyun Lee, Sam Lindley, Matija Pretnar, Xiaojia Rao, Andreas Rossberg, Sukyoung Ryu, Wonho Shin, Conrad Watt, Dongjun Youn
2022 B conf
Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk).
CONCUR
Philippa Gardner
2022 J jnl
Exact Separation Logic.
CoRR
Petar Maksimovic, Caroline Cronjäger, Julian Sutherland, Andreas Lööw, Sacha-Élie Ayoun, Philippa Gardner
2021 — conf
Gillian, Part II: Real-World Verification for JavaScript and C.
CAV (2)
Petar Maksimovic, Sacha-Élie Ayoun, José Fragoso Santos, Philippa Gardner
2021 J jnl
Gillian: A Multi-Language Platform for Unified Symbolic Analysis.
CoRR
Petar Maksimovic, José Fragoso Santos, Sacha-Élie Ayoun, Philippa Gardner
2021 J jnl
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs.
ACM Trans. Program. Lang. Syst.
Emanuele D'Osualdo, Julian Sutherland, Azadeh Farzan, Philippa Gardner
2021 B conf
Two Mechanisations of WebAssembly 1.0.
FM
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner
2020 J jnl
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact).
Dagstuhl Artifacts Ser.
Gabriela Sampaio, José Fragoso Santos, Petar Maksimovic, Philippa Gardner
2020 A conf
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications.
ECOOP
Gabriela Sampaio, José Fragoso Santos, Petar Maksimovic, Philippa Gardner
2020 A conf
Data Consistency in Transactional Storage Systems: A Centralised Semantics.
ECOOP
Shale Xiong, Andrea Cerone, Azalea Raad, Philippa Gardner
2020 A* conf
Gillian, part i: a multi-language platform for symbolic execution.
PLDI
José Fragoso Santos, Petar Maksimovic, Sacha-Élie Ayoun, Philippa Gardner
2020 J jnl
Gillian: Compositional Symbolic Execution for All.
CoRR
José Fragoso Santos, Petar Maksimovic, Sacha-Élie Ayoun, Philippa Gardner
2019 A conf
A Program Logic for First-Order Encapsulated WebAssembly.
ECOOP
Conrad Watt, Petar Maksimovic, Neelakantan R. Krishnaswami, Philippa Gardner
2019 J jnl
Data Consistency in Transactional Storage Systems: a Centralised Approach.
CoRR
Shale Xiong, Andrea Cerone, Azalea Raad, Philippa Gardner
2019 J jnl
JaVerT 2.0: compositional symbolic execution for JavaScript.
Proc. ACM Program. Lang.
José Fragoso Santos, Petar Maksimovic, Gabriela Cunha Sampaio, Philippa Gardner
2019 J jnl
Skeletal semantics and their interpretations.
Proc. ACM Program. Lang.
Martin Bodin, Philippa Gardner, Thomas P. Jensen, Alan Schmitt
2019 J jnl
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs.
CoRR
Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner, Julian Sutherland
2018 A conf
A Concurrent Specification of POSIX File Systems.
ECOOP
Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, Philippa Gardner
2018 J jnl
A Program Logic for First-Order Encapsulated WebAssembly.
CoRR
Conrad Watt, Petar Maksimovic, Neelakantan R. Krishnaswami, Philippa Gardner
2018 J jnl
A perspective on specifying and verifying concurrent modules.
J. Log. Algebraic Methods Program.
Thomas Dinsdale-Young, Pedro da Rocha Pinto, Philippa Gardner
2018 C conf
JaVerT: JavaScript Verification and Testing Framework: Invited Talk.
PPDP
Philippa Gardner
2018 J jnl
JaVerT: JavaScript verification toolchain.
Proc. ACM Program. Lang.
José Fragoso Santos, Petar Maksimovic, Daiva Naudziuniene, Thomas Wood, Philippa Gardner
2018 J jnl
Skeletal Semantics and their Interpretations.
CoRR
Martin Bodin, Philippa Gardner, Thomas P. Jensen, Alan Schmitt
2018 C conf
Symbolic Execution for JavaScript.
PPDP
José Fragoso Santos, Petar Maksimovic, Théotime Grohens, Julian Dolby, Philippa Gardner
2017 A conf
Abstract Specifications for Concurrent Maps.
ESOP
Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, Philippa Gardner
2017 A conf
Towards Logic-Based Verification of JavaScript Programs.
CADE
José Fragoso Santos, Philippa Gardner, Petar Maksimovic, Daiva Naudziuniene
2016 B conf
DOM: Specification and Client Reasoning.
APLAS
Azalea Raad, José Fragoso Santos, Philippa Gardner
2016 A conf
Modular Termination Verification for Non-blocking Concurrency.
ESOP
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, Julian Sutherland
2016 B conf
Verifying Concurrent Graph Algorithms.
APLAS
Azalea Raad, Aquinas Hobor, Jules Villard, Philippa Gardner
2015 — conf
A Trusted Mechanised Specification of JavaScript: One Year On.
CAV (1)
Philippa Gardner, Gareth Smith, Conrad Watt, Thomas Wood
2015 A conf
CoLoSL: Concurrent Local Subjective Logic.
ESOP
Azalea Raad, Jules Villard, Philippa Gardner
2015 J jnl
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).
Dagstuhl Reports
Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao
2015 B conf
Fault-Tolerant Resource Reasoning.
APLAS
Gian Ntzik, Pedro da Rocha Pinto, Philippa Gardner
2015 A conf
Reasoning about the POSIX file system: local update and global pathnames.
OOPSLA
Gian Ntzik, Philippa Gardner
2015 B conf
Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper).
MFPS
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner
2014 A* conf
A trusted mechanised JavaScript specification.
POPL
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith
2014 B conf
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap.
MFPS
Philippa Gardner, Azalea Raad, Mark J. Wheelhouse, Adam Wright
2014 A conf
Local Reasoning for the POSIX File System.
ESOP
Philippa Gardner, Gian Ntzik, Adam Wright
2014 A conf
TaDA: A Logic for Time and Data Abstraction.
ECOOP
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner
2013 A ed.
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
ESOP
Matthias Felleisen, Philippa Gardner
2013 A* conf
Views: compositional reasoning for concurrent programs.
POPL
Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang
2012 J jnl
Processes in space.
Theor. Comput. Sci.
Luca Cardelli, Philippa Gardner
2012 A* conf
Towards a program logic for JavaScript.
POPL
Philippa Gardner, Sergio Maffeis, Gareth David Smith
2011 A conf
A simple abstraction for complex concurrent indexes.
OOPSLA
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Mark J. Wheelhouse
2011 B conf
Abstract Local Reasoning for Program Modules.
CALCO
Thomas Dinsdale-Young, Philippa Gardner, Mark J. Wheelhouse
2010 — conf
Abstraction and Refinement for Local Reasoning.
VSTTE
Thomas Dinsdale-Young, Philippa Gardner, Mark J. Wheelhouse
2010 J jnl
Adjunct elimination in Context Logic for trees.
Inf. Comput.
Cristiano Calcagno, Thomas Dinsdale-Young, Philippa Gardner
2010 A conf
Concurrent Abstract Predicates.
ECOOP
Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis
2010 C conf
Processes in Space.
CiE
Luca Cardelli, Philippa Gardner
2010 — conf
Reasoning about client-side web programs: invited talk.
EDBT/ICDT Workshops
Philippa Gardner
2010 J jnl
Report on the EDBT/ICDT 2010 workshop on updates in XML.
SIGMOD Rec.
Michael Benedikt, Daniela Florescu, Philippa Gardner, Giovanna Guerrini, Marco Mesiti, Emmanuel Waller
2009 J jnl
A process model of Rho GTP-binding proteins.
Theor. Comput. Sci.
Luca Cardelli, Emmanuelle Caron, Philippa Gardner, Ozan Kahramanogullari, Andrew Phillips
2009 A conf
Automatic Parallelization with Separation Logic.
ESOP
Mohammad Raza, Cristiano Calcagno, Philippa Gardner
2009 — ed.
Database Programming Languages - DBPL 2009, 12th International Symposium, Lyon, France, August 24, 2009. Proceedings
DBPL
Philippa Gardner, Floris Geerts
2009 J jnl
Footprints in Local Reasoning
Log. Methods Comput. Sci.
Mohammad Raza, Philippa Gardner
2009 — conf
Small Specifications for Tree Update.
WS-FM
Philippa Gardner, Mark J. Wheelhouse
2008 — conf
A Process Model of Actin Polymerisation.
FBTC@ICALP
Luca Cardelli, Emmanuelle Caron, Philippa Gardner, Ozan Kahramanogullari, Andrew Phillips
2008 J jnl
Behavioural equivalences for dynamic Web data.
J. Log. Algebraic Methods Program.
Sergio Maffeis, Philippa Gardner
2008 — conf
DOM: Towards a Formal Specification.
PLAN-X
Philippa Gardner, Gareth Smith, Mark J. Wheelhouse, Uri Zarfaty
2008 B conf
Footprints in Local Reasoning.
FoSSaCS
Mohammad Raza, Philippa Gardner
2008 A* conf
Local Hoare reasoning about DOM.
PODS
Philippa Gardner, Gareth Smith, Mark J. Wheelhouse, Uri Zarfaty
2007 — conf
A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis.
FBTC@CONCUR
Luca Cardelli, Philippa Gardner, Ozan Kahramanogullari
2007 B conf
Adjunct Elimination in Context Logic for Trees.
APLAS
Cristiano Calcagno, Thomas Dinsdale-Young, Philippa Gardner
2007 C conf
An Introduction to Context Logic.
WoLLIC
Philippa Gardner, Uri Zarfaty
2007 A* conf
Context logic as modal logic: completeness and parametric inexpressivity.
POPL
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
2007 J jnl
Expressiveness and complexity of graph logic.
Inf. Comput.
Anuj Dawar, Philippa Gardner, Giorgio Ghelli
2007 J jnl
Linear forwarders.
Inf. Comput.
Philippa Gardner, Cosimo Laneve, Lucian Wischik
2007 — conf
Local Reasoning about Data Update.
Computation, Meaning, and Logic
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
2007 — conf
Manipulating Trees with Hidden Labels.
Computation, Meaning, and Logic
Luca Cardelli, Philippa Gardner, Giorgio Ghelli
2006 J jnl
Editorial.
Theor. Comput. Sci.
Philippa Gardner, Nobuko Yoshida
2006 B conf
Local Reasoning About Tree Update.
MFPS
Uri Zarfaty, Philippa Gardner
2005 A* conf
Context logic and tree update.
POPL
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
2005 J jnl
Explicit fusions.
Theor. Comput. Sci.
Lucian Wischik, Philippa Gardner
2005 B conf
From Separation Logic to First-Order Logic.
FoSSaCS
Cristiano Calcagno, Philippa Gardner, Matthew Hague
2005 — ed.
Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6.-11. June 2004
Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems
Barbara König, Ugo Montanari, Philippa Gardner
2005 J jnl
Modelling dynamic web data.
Theor. Comput. Sci.
Philippa Gardner, Sergio Maffeis
2004 — conf
04241 Abstracts Collection - Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems.
Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems
Barbara König, Ugo Montanari, Philippa Gardner
2004 — conf
Adjunct Elimination Through Games in Static Ambient Logic.
FSTTCS
Anuj Dawar, Philippa Gardner, Giorgio Ghelli
2004 — conf
Behavioural Equivalences for Dynamic Web Data.
IFIP TCS
Sergio Maffeis, Philippa Gardner
2004 B ed.
CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings
CONCUR
Philippa Gardner, Nobuko Yoshida
2004 B conf
Strong Bisimulation for the Explicit Fusion Calculus.
FoSSaCS
Lucian Wischik, Philippa Gardner
2003 B conf
Linear Forwarders.
CONCUR
Philippa Gardner, Cosimo Laneve, Lucian Wischik
2003 B conf
Manipulating Trees with Hidden Labels.
FoSSaCS
Luca Cardelli, Philippa Gardner, Giorgio Ghelli
2003 — conf
Modelling Dynamic Web Data.
DBPL
Philippa Gardner, Sergio Maffeis
2002 A* conf
A Spatial Logic for Querying Graphs.
ICALP
Luca Cardelli, Philippa Gardner, Giorgio Ghelli
2002 B conf
The Fusion Machine.
CONCUR
Philippa Gardner, Cosimo Laneve, Lucian Wischik
2000 B conf
Explicit Fusions.
MFCS
Philippa Gardner, Lucian Wischik
2000 B conf
From Process Calculi to Process Frameworks.
CONCUR
Philippa Gardner
1999 J jnl
Closed Action Calculi.
Theor. Comput. Sci.
Philippa Gardner
1997 — conf
A Type-theoretic Description of Action Calculi.
HOOTS
Philippa Gardner
1997 B conf
From Action Calculi to Linear Logic.
CSL
Andrew G. Barber, Philippa Gardner, Masahito Hasegawa, Gordon D. Plotkin
1997 — conf
Types and Models for Higher-Order Action Calculi.
TACS
Philippa Gardner, Masahito Hasegawa
1995 B conf
A name-free account of action calculi.
MFPS
Philippa Gardner
1995 J jnl
Equivalences between Logics and Their Representing Type Theories.
Math. Struct. Comput. Sci.
Philippa Gardner
1994 — conf
Discovering Needed Reductions Using Type Theory.
TACS
Philippa Gardner
1993 B conf
A New Type Theory for Representing Logics.
LPAR
Philippa Gardner
1992 — —
Representing logics in type theory.
Philippa Gardner
1991 — conf
Unfold/Fold Transformations of Logic Programs.
Computational Logic - Essays in Honor of Alan Robinson
Philippa Gardner, John C. Shepherdson