Matthew J. Parkinson

Publication Activity (10 Years)

Years Active: 2003-2024
Publications (10 Years): 18

Top Topics

Predicate Logic

Memory Management

Top Venues

Proc. ACM Program. Lang.

Publications

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