Matthew J. Parkinson

According to our database, Matthew J. Parkinson authored at least 52 papers between 2003 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

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., October, 2023

Reference Capabilities for Flexible Memory Management.

Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad

Proc. ACM Program. Lang., October, 2023

Reference Capabilities for Flexible Memory Management: Extended Version.

Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad

CoRR, 2023

Wait-Free Weak Reference Counting.

Matthew J. Parkinson, Sylvan Clebsch, Ben Simner

Proceedings of the 2023 ACM SIGPLAN International Symposium on Memory Management, 2023

2019

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

Proceedings of the 2019 ACM SIGPLAN International Symposium on Memory Management, 2019

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

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

Proving Linearizability Using Partial Orders (Extended Version).

Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson

CoRR, 2017

Simple, fast, and safe manual memory management.

Piyus Kedia, Manuel Costa, Matthew J. Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Aaron Blankstein

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Proving Linearizability Using Partial Orders.

Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson

Proceedings of the Programming Languages and Systems, 2017

Starling: Lightweight Concurrency Verification with Views.

Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

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

A Generic Logic for Proving Linearizability (Extended Version).

Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson

CoRR, 2016

A Generic Logic for Proving Linearizability.

Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson

Proceedings of the FM 2016: Formal Methods, 2016

2015

New Lace and Arsenic: adventures in weak memory with a program logic.

Richard Bornat, Jade Alglave, Matthew J. Parkinson

CoRR, 2015

The Push/Pull model of transactions.

Eric Koskinen, Matthew J. Parkinson

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2013

Separation Logic for Object-Oriented Programming.

Matthew J. Parkinson, Gavin M. Bierman

Proceedings of the Aliasing in Object-Oriented Programming. Types, 2013

Views: compositional reasoning for concurrent programs.

Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Ribbon Proofs for Separation Logic.

John Wickerson, Mike Dodds, Matthew J. Parkinson

Proceedings of the Programming Languages and Systems, 2013

Modular Reasoning about Separation of Concurrent Data Structures.

Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson

Proceedings of the Programming Languages and Systems, 2013

Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library.

Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson

Proceedings of the ECOOP 2013 - Object-Oriented Programming, 2013

SeLoger: A Tool for Graph-Based Reasoning in Separation Logic.

Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Behavioral interface specification languages.

John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson

ACM Comput. Surv., 2012

The Relationship Between Separation Logic and Implicit Dynamic Frames

Matthew J. Parkinson, Alexander J. Summers

Log. Methods Comput. Sci., 2012

Uniqueness and reference immutability for safe parallelism.

Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

2011

Lightweight Java.

Rok Strnisa, Matthew J. Parkinson

Arch. Formal Proofs, 2011

jStar-eclipse: an IDE for automated verification of Java programs.

Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Matthew J. Parkinson

Proceedings of the SIGSOFT/FSE'11 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19) and ESEC'11: 13th European Software Engineering Conference (ESEC-13), 2011

Automatic safety proofs for asynchronous memory operations.

Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson

Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2011

Modular reasoning for deterministic parallelism.

Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Safe asynchronous multicore memory operations.

Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson

Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011

Tractable Reasoning in a Fragment of Separation Logic.

Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

2010

The Next 700 Separation Logics - (Invited Paper).

Matthew J. Parkinson

Proceedings of the Verified Software: Theories, 2010

Coarse-grained transactions.

Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Explicit Stabilisation for Modular Rely-Guarantee Reasoning.

John Wickerson, Mike Dodds, Matthew J. Parkinson

Proceedings of the Programming Languages and Systems, 2010

Verifying Generics and Delegates.

Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson

Proceedings of the ECOOP 2010, 2010

Concurrent Abstract Predicates.

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis

Proceedings of the ECOOP 2010, 2010

2009

Separation Logic Verification of C Programs with an SMT Solver.

Matko Botincan, Matthew J. Parkinson, Wolfram Schulte

Proceedings of the 4th International Workshop on Systems Software Verification, 2009

Proving that non-blocking algorithms don't block.

Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Deny-Guarantee Reasoning.

Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis

Proceedings of the Programming Languages and Systems, 2009

2008

Separation logic, abstraction and inheritance.

Matthew J. Parkinson, Gavin M. Bierman

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

jStar: towards practical verification for java.

Dino Distefano, Matthew J. Parkinson

Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2008

From Java To UpgradeJ: An Empirical Study.

Ewan D. Tempero, Gavin M. Bierman, James Noble, Matthew J. Parkinson

Proceedings of the 1st ACM Workshop on Hot Topics in Software Upgrades, 2008

UpgradeJ: Incremental Typechecking for Class Upgrades.

Gavin M. Bierman, Matthew J. Parkinson, James Noble

Proceedings of the ECOOP 2008, 2008

2007

Modular Safety Checking for Fine-Grained Concurrency.

Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis

Proceedings of the Static Analysis, 14th International Symposium, 2007

Modular verification of a non-blocking stack.

Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

The java module system: core design and semantic definition.

Rok Strnisa, Peter Sewell, Matthew J. Parkinson

Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

A Marriage of Rely/Guarantee and Separation Logic.

Viktor Vafeiadis, Matthew J. Parkinson

Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

2006

Local reasoning for Java.

Matthew J. Parkinson

PhD thesis, 2006

Variables as Resource in Hoare Logics.

Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

2005

Separation logic and abstraction.

Matthew J. Parkinson, Gavin M. Bierman

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Permission accounting in separation logic.

Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

2003

Effects and effect inference for a core Java calculus.

Gavin M. Bierman, Matthew J. Parkinson

Proceedings of the Workshop on Object Oriented Developments, 2003