Philippa Gardner

ORCID

Publication Activity (10 Years)

Years Active: 1991-2024
Publications (10 Years): 35

Top Venues

CoRR

ECOOP

Proc. ACM Program. Lang.

ESOP

University of Edinburgh, UK (PHD)

Education History

University of Edinburgh, UK

PHD

Publications

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

Philippa Gardner.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Philippa Gardner