Effects and effect inference for a core Java calculus. - Gavin M. Bierman; Matthew J. Parkinson (WOOD, 2003)

Permission accounting in separation logic. - Richard Bornat; Cristiano Calcagno; Peter W. O'Hearn; Matthew J. Parkinson (POPL, 2005)

Separation logic and abstraction. - Matthew J. Parkinson; Gavin M. Bierman (POPL, 2005)

Variables as Resource in Hoare Logics. - Matthew J. Parkinson; Richard Bornat; Cristiano Calcagno (LICS, 2006)

Local reasoning for Java. - Matthew J. Parkinson (2006)

A Marriage of Rely/Guarantee and Separation Logic. - Viktor Vafeiadis; Matthew J. Parkinson (CONCUR, 2007)

The java module system: core design and semantic definition. - Rok Strnisa; Peter Sewell; Matthew J. Parkinson (OOPSLA, 2007)

Modular verification of a non-blocking stack. - Matthew J. Parkinson; Richard Bornat; Peter W. O'Hearn (POPL, 2007)

Modular Safety Checking for Fine-Grained Concurrency. - Cristiano Calcagno; Matthew J. Parkinson; Viktor Vafeiadis (SAS, 2007)

UpgradeJ: Incremental Typechecking for Class Upgrades. - Gavin M. Bierman; Matthew J. Parkinson; James Noble 001 (ECOOP, 2008)

From Java To UpgradeJ: An Empirical Study. - Ewan D. Tempero; Gavin M. Bierman; James Noble 001; Matthew J. Parkinson (HotSWUp, 2008)

jStar: towards practical verification for java. - Dino Distefano; Matthew J. Parkinson (OOPSLA, 2008)

Separation logic, abstraction and inheritance. - Matthew J. Parkinson; Gavin M. Bierman (POPL, 2008)

Deny-Guarantee Reasoning. - Mike Dodds; Xinyu Feng 001; Matthew J. Parkinson; Viktor Vafeiadis (ESOP, 2009)

Proving that non-blocking algorithms don't block. - Alexey Gotsman; Byron Cook; Matthew J. Parkinson; Viktor Vafeiadis (POPL, 2009)

Separation Logic Verification of C Programs with an SMT Solver. - Matko Botincan; Matthew J. Parkinson; Wolfram Schulte (SSV, 2009)

Concurrent Abstract Predicates. - Thomas Dinsdale-Young; Mike Dodds; Philippa Gardner; Matthew J. Parkinson; Viktor Vafeiadis (ECOOP, 2010)

Verifying Generics and Delegates. - Kasper Svendsen; Lars Birkedal; Matthew J. Parkinson (ECOOP, 2010)

Explicit Stabilisation for Modular Rely-Guarantee Reasoning. - John Wickerson; Mike Dodds; Matthew J. Parkinson (ESOP, 2010)

Coarse-grained transactions. - Eric Koskinen; Matthew J. Parkinson; Maurice Herlihy (POPL, 2010)

The Next 700 Separation Logics - (Invited Paper). - Matthew J. Parkinson (VSTTE, 2010)

Tractable Reasoning in a Fragment of Separation Logic. - Byron Cook; Christoph Haase; Joël Ouaknine; Matthew J. Parkinson; James Worrell 001 (CONCUR, 2011)

The Relationship between Separation Logic and Implicit Dynamic Frames. - Matthew J. Parkinson; Alexander J. Summers (ESOP, 2011)

Safe asynchronous multicore memory operations. - Matko Botincan; Mike Dodds; Alastair F. Donaldson; Matthew J. Parkinson (ASE, 2011)

Modular reasoning for deterministic parallelism. - Mike Dodds; Suresh Jagannathan; Matthew J. Parkinson (POPL, 2011)

Automatic safety proofs for asynchronous memory operations. - Matko Botincan; Mike Dodds; Alastair F. Donaldson; Matthew J. Parkinson (PPoPP, 2011)

jStar-eclipse: an IDE for automated verification of Java programs. - Daiva Naudziuniene; Matko Botincan; Dino Distefano; Mike Dodds; Radu Grigore; Matthew J. Parkinson (SIGSOFT FSE, 2011)

Lightweight Java. - Rok Strnisa; Matthew J. Parkinson (Arch. Formal Proofs, 2011)

Uniqueness and reference immutability for safe parallelism. - Colin S. Gordon; Matthew J. Parkinson; Jared Parsons; Aleks Bromfield; Joe Duffy (OOPSLA, 2012)

Behavioral interface specification languages. - John Hatcliff; Gary T. Leavens; K. Rustan M. Leino; Peter Müller 001; Matthew J. Parkinson (ACM Comput. Surv., 2012)

SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. - Christoph Haase; Samin Ishtiaq; Joël Ouaknine; Matthew J. Parkinson (CAV, 2013)

Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library. - Kasper Svendsen; Lars Birkedal; Matthew J. Parkinson (ECOOP, 2013)

Modular Reasoning about Separation of Concurrent Data Structures. - Kasper Svendsen; Lars Birkedal; Matthew J. Parkinson (ESOP, 2013)

Ribbon Proofs for Separation Logic. - John Wickerson; Mike Dodds; Matthew J. Parkinson (ESOP, 2013)

Views: compositional reasoning for concurrent programs. - Thomas Dinsdale-Young; Lars Birkedal; Philippa Gardner; Matthew J. Parkinson; Hongseok Yang (POPL, 2013)

Separation Logic for Object-Oriented Programming. - Matthew J. Parkinson; Gavin M. Bierman (Aliasing in Object-Oriented Programming, 2013)

The Push/Pull model of transactions. - Eric Koskinen; Matthew J. Parkinson (PLDI, 2015)

New Lace and Arsenic: adventures in weak memory with a program logic. - Richard Bornat; Jade Alglave; Matthew J. Parkinson (CoRR, 2015)

A Generic Logic for Proving Linearizability. - Artem Khyzha; Alexey Gotsman; Matthew J. Parkinson (FM, 2016)

A Generic Logic for Proving Linearizability (Extended Version). - Artem Khyzha; Alexey Gotsman; Matthew J. Parkinson (CoRR, 2016)

Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic. - Mike Dodds; Suresh Jagannathan; Matthew J. Parkinson; Kasper Svendsen; Lars Birkedal (ACM Trans. Program. Lang. Syst., 2016)

Starling: Lightweight Concurrency Verification with Views. - Matt Windsor; Mike Dodds; Ben Simner; Matthew J. Parkinson (CAV (1), 2017)

Proving Linearizability Using Partial Orders. - Artem Khyzha; Mike Dodds; Alexey Gotsman; Matthew J. Parkinson (ESOP, 2017)

Simple, fast, and safe manual memory management. - Piyus Kedia; Manuel Costa; Matthew J. Parkinson; Kapil Vaswani; Dimitrios Vytiniotis; Aaron Blankstein (PLDI, 2017)

Proving Linearizability Using Partial Orders (Extended Version). - Artem Khyzha; Mike Dodds; Alexey Gotsman; Matthew J. Parkinson (CoRR, 2017)

Project snowflake: non-blocking safe manual memory management in .NET. - Matthew J. Parkinson; Dimitrios Vytiniotis; Kapil Vaswani; Manuel Costa; Pantazis Deligiannis; Dylan McDermott; Aaron Blankstein; Jonathan Balkind (Proc. ACM Program. Lang., 2017)

Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types. - Colin S. Gordon; Michael D. Ernst; Dan Grossman; Matthew J. Parkinson (ACM Trans. Program. Lang. Syst., 2017)

snmalloc: a message passing allocator. - Paul Liétar; Theodore Butler; Sylvan Clebsch; Sophia Drossopoulou; Juliana Franco; Matthew J. Parkinson; Alex Shamis; Christoph M. Wintersteiger; David Chisnall (ISMM, 2019)

Wait-Free Weak Reference Counting. - Matthew J. Parkinson; Sylvan Clebsch; Ben Simner (ISMM, 2023)

Reference Capabilities for Flexible Memory Management: Extended Version. - Ellen Arvidsson; Elias Castegren; Sylvan Clebsch; Sophia Drossopoulou; James Noble 001; Matthew J. Parkinson; Tobias Wrigstad (CoRR, 2023)

Reference Capabilities for Flexible Memory Management. - Ellen Arvidsson; Elias Castegren; Sylvan Clebsch; Sophia Drossopoulou; James Noble 001; Matthew J. Parkinson; Tobias Wrigstad (Proc. ACM Program. Lang., 2023)

When Concurrency Matters: Behaviour-Oriented Concurrency. - Luke Cheeseman; Matthew J. Parkinson; Sylvan Clebsch; Marios Kogias; Sophia Drossopoulou; David Chisnall; Tobias Wrigstad; Paul Liétar (Proc. ACM Program. Lang., 2023)

Concurrent Immediate Reference Counting (Abstract). - Jaehwang Jung; Jeonghyeon Kim; Matthew J. Parkinson; Jeehoon Kang (HOPC@SPAA, 2024)

BatchIt: Optimizing Message-Passing Allocators for Producer-Consumer Workloads: An Intellectual Abstract. - Nathaniel Wesley Filardo; Matthew J. Parkinson (ISMM, 2024)

Reference Counting Deeply Immutable Data Structures with Cycles: An Intellectual Abstract. - Matthew J. Parkinson; Sylvan Clebsch; Tobias Wrigstad (ISMM, 2024)

Trieste: A C++ DSL for Flexible Tree Rewriting. - Sylvan Clebsch; Matilda Blomqvist; Elias Castegren; Matthew A. Johnson 003; Matthew J. Parkinson (SLE, 2024)

Concurrent Immediate Reference Counting. - Jaehwang Jung; Jeonghyeon Kim; Matthew J. Parkinson; Jeehoon Kang (Proc. ACM Program. Lang., 2024)

DORADD: Deterministic Parallel Execution in the Era of Microsecond-Scale Computing. - Zhengqing Liu; Musa Unal; Matthew J. Parkinson; Marios Kogias (PPoPP, 2025)

Dynamic Region Ownership for Concurrency Safety. - Fridtjof Peer Stoldt; Gary Brandt Bucher II; Sylvan Clebsch; Matthew A. Johnson 003; Matthew J. Parkinson; Guido van Rossum; Eric Snow; Tobias Wrigstad (Proc. ACM Program. Lang., 2025)