Matthew J. Parkinson

61 papers A* 13A 13B 7C 4Journal 14Unranked 8
YearRankTypeTitle / Venue / Authors
2026 — conf
Decoupling Isolation and Concurrency: An Actor-Centric View of Behaviour-Oriented Concurrency.
Concurrent Programming, Open Systems and Formal Methods
Luke Cheeseman, Elias Castegren, Sophia Drossopoulou, Tobias Wrigstad, Sylvan Clebsch, Matthew J. Parkinson
2025 B conf
DORADD: Deterministic Parallel Execution in the Era of Microsecond-Scale Computing.
PPoPP
Zhengqing Liu, Musa Unal, Matthew J. Parkinson, Marios Kogias
2025 J jnl
Dynamic Region Ownership for Concurrency Safety.
Proc. ACM Program. Lang.
Fridtjof Peer Stoldt, Gary Brandt Bucher II, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Guido van Rossum, Eric Snow, Tobias Wrigstad
2024 C conf
BatchIt: Optimizing Message-Passing Allocators for Producer-Consumer Workloads: An Intellectual Abstract.
ISMM
Nathaniel Wesley Filardo, Matthew J. Parkinson
2024 — conf
Concurrent Immediate Reference Counting (Abstract).
HOPC@SPAA
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang
2024 J jnl
Concurrent Immediate Reference Counting.
Proc. ACM Program. Lang.
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang
2024 C conf
Reference Counting Deeply Immutable Data Structures with Cycles: An Intellectual Abstract.
ISMM
Matthew J. Parkinson, Sylvan Clebsch, Tobias Wrigstad
2024 B conf
Trieste: A C++ DSL for Flexible Tree Rewriting.
SLE
Sylvan Clebsch, Matilda Blomqvist, Elias Castegren, Matthew A. Johnson, Matthew J. Parkinson
2023 J jnl
Reference Capabilities for Flexible Memory Management.
Proc. ACM Program. Lang.
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad
2023 J jnl
Reference Capabilities for Flexible Memory Management: Extended Version.
CoRR
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad
2023 C conf
Wait-Free Weak Reference Counting.
ISMM
Matthew J. Parkinson, Sylvan Clebsch, Ben Simner
2023 J jnl
When Concurrency Matters: Behaviour-Oriented Concurrency.
Proc. ACM Program. Lang.
Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad, Paul Liétar
2019 C conf
snmalloc: a message passing allocator.
ISMM
Paul Liétar, Theodore Butler, Sylvan Clebsch, Sophia Drossopoulou, Juliana Franco, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger, David Chisnall
2017 J jnl
Project snowflake: non-blocking safe manual memory management in .NET.
Proc. ACM Program. Lang.
Matthew J. Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott, Aaron Blankstein, Jonathan Balkind
2017 J jnl
Proving Linearizability Using Partial Orders (Extended Version).
CoRR
Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson
2017 A conf
Proving Linearizability Using Partial Orders.
ESOP
Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson
2017 A* conf
Simple, fast, and safe manual memory management.
PLDI
Piyus Kedia, Manuel Costa, Matthew J. Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Aaron Blankstein
2017 — conf
Starling: Lightweight Concurrency Verification with Views.
CAV (1)
Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson
2017 J jnl
Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types.
ACM Trans. Program. Lang. Syst.
Colin S. Gordon, Michael D. Ernst, Dan Grossman, Matthew J. Parkinson
2016 J jnl
A Generic Logic for Proving Linearizability (Extended Version).
CoRR
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
2016 B conf
A Generic Logic for Proving Linearizability.
FM
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
2016 J jnl
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic.
ACM Trans. Program. Lang. Syst.
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal
2015 J jnl
New Lace and Arsenic: adventures in weak memory with a program logic.
CoRR
Richard Bornat, Jade Alglave, Matthew J. Parkinson
2015 A* conf
The Push/Pull model of transactions.
PLDI
Eric Koskinen, Matthew J. Parkinson
2013 A conf
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library.
ECOOP
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
2013 A conf
Modular Reasoning about Separation of Concurrent Data Structures.
ESOP
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
2013 A conf
Ribbon Proofs for Separation Logic.
ESOP
John Wickerson, Mike Dodds, Matthew J. Parkinson
2013 A* conf
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic.
CAV
Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson
2013 — ch.
Separation Logic for Object-Oriented Programming.
Aliasing in Object-Oriented Programming
Matthew J. Parkinson, Gavin M. Bierman
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
Behavioral interface specification languages.
ACM Comput. Surv.
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
2012 J jnl
The Relationship Between Separation Logic and Implicit Dynamic Frames
Log. Methods Comput. Sci.
Matthew J. Parkinson, Alexander J. Summers
2012 A conf
Uniqueness and reference immutability for safe parallelism.
OOPSLA
Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy
2011 B conf
Automatic safety proofs for asynchronous memory operations.
PPoPP
Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson
2011 J jnl
Lightweight Java.
Arch. Formal Proofs
Rok Strnisa, Matthew J. Parkinson
2011 A* conf
Modular reasoning for deterministic parallelism.
POPL
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson
2011 A* conf
Safe asynchronous multicore memory operations.
ASE
Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson
2011 A conf
The Relationship between Separation Logic and Implicit Dynamic Frames.
ESOP
Matthew J. Parkinson, Alexander J. Summers
2011 B conf
Tractable Reasoning in a Fragment of Separation Logic.
CONCUR
Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell
2011 — conf
jStar-eclipse: an IDE for automated verification of Java programs.
SIGSOFT FSE
Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Matthew J. Parkinson
2010 A* conf
Coarse-grained transactions.
POPL
Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy
2010 A conf
Concurrent Abstract Predicates.
ECOOP
Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis
2010 A conf
Explicit Stabilisation for Modular Rely-Guarantee Reasoning.
ESOP
John Wickerson, Mike Dodds, Matthew J. Parkinson
2010 — conf
The Next 700 Separation Logics - (Invited Paper).
VSTTE
Matthew J. Parkinson
2010 A conf
Verifying Generics and Delegates.
ECOOP
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
2009 A conf
Deny-Guarantee Reasoning.
ESOP
Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis
2009 A* conf
Proving that non-blocking algorithms don't block.
POPL
Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
2009 — conf
Separation Logic Verification of C Programs with an SMT Solver.
SSV
Matko Botincan, Matthew J. Parkinson, Wolfram Schulte
2008 — conf
From Java To UpgradeJ: An Empirical Study.
HotSWUp
Ewan D. Tempero, Gavin M. Bierman, James Noble, Matthew J. Parkinson
2008 A* conf
Separation logic, abstraction and inheritance.
POPL
Matthew J. Parkinson, Gavin M. Bierman
2008 A conf
UpgradeJ: Incremental Typechecking for Class Upgrades.
ECOOP
Gavin M. Bierman, Matthew J. Parkinson, James Noble
2008 A conf
jStar: towards practical verification for java.
OOPSLA
Dino Distefano, Matthew J. Parkinson
2007 B conf
A Marriage of Rely/Guarantee and Separation Logic.
CONCUR
Viktor Vafeiadis, Matthew J. Parkinson
2007 B conf
Modular Safety Checking for Fine-Grained Concurrency.
SAS
Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis
2007 A* conf
Modular verification of a non-blocking stack.
POPL
Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn
2007 A conf
The java module system: core design and semantic definition.
OOPSLA
Rok Strnisa, Peter Sewell, Matthew J. Parkinson
2006 — —
Local reasoning for Java.
Matthew J. Parkinson
2006 A* conf
Variables as Resource in Hoare Logics.
LICS
Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno
2005 A* conf
Permission accounting in separation logic.
POPL
Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson
2005 A* conf
Separation logic and abstraction.
POPL
Matthew J. Parkinson, Gavin M. Bierman
2003 — conf
Effects and effect inference for a core Java calculus.
WOOD
Gavin M. Bierman, Matthew J. Parkinson