BatchIt: Optimizing Message-Passing Allocators for Producer-Consumer Workloads: An Intellectual Abstract
Nathaniel Filardo, Matthew J. Parkinson
Proceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management (ISMM'24) | June 2024
Matthew Parkinson
Principal Researcher
Publications
Publications by Year
-
Reference Counting Deeply Immutable Data Structures with Cycles: an Intellectual Abstract
Matthew J. Parkinson, Sylvan Clebsch, Tobias Wrigstad
n Proceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management (ISMM ’24) | June 2024
Concurrent Immediate Reference Counting
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang
PACM PL | June 2024
-
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, Vol 7(OOPSLA2)
Reference Capabilities for Flexible Memory Management
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, Matthew J. Parkinson, James Noble, Tobias Wrigstad
Proc. ACM Program. Lang. | October 2023, Vol 7(OOPSLA2)
Wait-Free Weak Reference Counting
Matthew J. Parkinson, Sylvan Clebsch, Ben Simner
ACM SIGPLAN International Symposium on Memory Management | June 2023
-
Nekara: Generalized Concurrency Testing
Udit Agarwal, Pantazis Deligiannis, Cheng Huang, Kumseok Jung, Akash Lal, Immad Naseer, Matthew J. Parkinson, Arun Thangamani, Jyothi Vedurada, Yunpeng Xiao
2021 Automated Software Engineering | November 2021
-
snmalloc: A message passing Allocator
David Chisnall, Sylvan Clebsch, Sophia Drossopoulou, Juliana Vicente Franco, Paul Lietar, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger
ISSM | June 2019, pp. 122-135
-
Project Snowflake: Non-blocking safe manual memory management in .NET
Matthew J. Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Manuel Costa, Pantazis Deligiannis, Aaron Blankstein, Dylan McDermott, Jonathan Balkind
MSR-TR-2017-32 | July 2017
Published by Microsoft
Starling: Lightweight Concurrency Verification with Views
Matt Windsor, Mike Dodds, Ben Simner, Matthew Parkinson
Computer Aided Verification 2017 | July 2017
Proving Linearizability Using Partial Orders (Extended Version)
Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson
July 2017
Simple, Fast and Safe Manual Memory Management
Piyus Kedia, Manuel Costa, Dimitrios Vytiniotis, Matthew J. Parkinson, Kapil Vaswani, Aaron Blankstein
Proceedings of the Conference on Programming Langauges Design and Implementation (PLDI) | June 2017
The F# Language Design RFCs (F# 4.0, 4.1)
Don Syme, Matthew J. Parkinson
May 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 Transactions on Programming Languages and Systems | May 2017, Vol 39(3)
-
A Generic Logic for Proving Linearizability
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
International Symposium on Formal Methods | November 2016
New Lace and Arsenic: adventures in weak memory with a program logic
Richard Bornat, Jade Alglave, Matthew J. Parkinson
November 2016
Matthew Parkinson
A Generic Logic for Proving Linearizability (Extended Version)
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
September 2016
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal
ACM Transactions on Programming Languages and Systems | January 2016, Vol 38(2)
-
The Push/Pull model of transactions
Eric Koskinen, Matthew J. Parkinson
ACM SIGPLAN Notices | June 2015, Vol 50(6): pp. 186-195
-
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
ECOOP 2013 - Object-Oriented Programming - 27th European Conference, Montpellier, France, July 1-5, 2013. Proceedings | August 2013
Separation Logic for Object-Oriented Programming
Matthew J. Parkinson, Gavin Bierman
Aliasing in Object-Oriented Programming. Types, Analysis and Verification | Published by Springer | 2013, Vol 7850 | Aliasing in Object-Oriented Programming. Types, Analysis and Verification edition
Modular Reasoning about Separation for Concurrent Data Structures
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
Proceedings of ESOP | January 2013
Ribbon Proofs for Separation Logic
John Wickerson, Mike Dodds, Matthew J. Parkinson
Proceedings of ESOP | January 2013
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
Christoph Haase, Samin Ishtiaq, Joel Ouaknine, Matthew J. Parkinson
Computer Aided Verification (CAV) | January 2013
Views: Compositional Reasoning for Concurrent Programs
Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang
Proceedings of POPL | January 2013
-
Uniqueness and Reference Immutability for Safe Parallelism
Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy
MSR-TR-2012-79 | October 2012
The Relationship Between Separation Logic and Implicit Dynamic Frames
Matthew J. Parkinson, Alexander J. Summers
Logical Methods in Computer Science | January 2012, Vol 8(3)
-
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 | January 2011
-
The Next 700 Separation Logics
2010 Verified Software: Theories, Tools, Experiments | August 2010
10.1007/978-3-642-15057-9_12
Coarse-grained transactions
Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | January 2010
ISBN: 978-1-60558-479-9
-
Proving that non-blocking algorithms don’t block
Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
SIGPLAN Notices | January 2009, Vol 44(1): pp. 16-28
-
UpgradeJ: Incremental Typechecking for Class Upgrades
Gavin Bierman, Matthew J. Parkinson, James Noble
Proceedings of the 22nd European conference on Object-Oriented Programming | January 2008
ISBN: 978-3-540-70591-8
-
The java module system: core design and semantic definition
Rok Strniša, Peter Sewell, Matthew J. Parkinson
Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications | January 2007
ISBN: 978-1-59593-786-5
-
Local Reasoning for Java
January 2005
January 2005
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-654.html
Separation logic and abstraction
Matthew J. Parkinson, Gavin Bierman
POPL '05 Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | January 2005
Publications by Research Area
-
BatchIt: Optimizing Message-Passing Allocators for Producer-Consumer Workloads: An Intellectual Abstract
Nathaniel Filardo, Matthew J. Parkinson
Proceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management (ISMM'24) | June 2024
Reference Counting Deeply Immutable Data Structures with Cycles: an Intellectual Abstract
Matthew J. Parkinson, Sylvan Clebsch, Tobias Wrigstad
n Proceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management (ISMM ’24) | June 2024
Concurrent Immediate Reference Counting
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang
PACM PL | June 2024
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, Vol 7(OOPSLA2)
Reference Capabilities for Flexible Memory Management
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, Matthew J. Parkinson, James Noble, Tobias Wrigstad
Proc. ACM Program. Lang. | October 2023, Vol 7(OOPSLA2)
Wait-Free Weak Reference Counting
Matthew J. Parkinson, Sylvan Clebsch, Ben Simner
ACM SIGPLAN International Symposium on Memory Management | June 2023
Nekara: Generalized Concurrency Testing
Udit Agarwal, Pantazis Deligiannis, Cheng Huang, Kumseok Jung, Akash Lal, Immad Naseer, Matthew J. Parkinson, Arun Thangamani, Jyothi Vedurada, Yunpeng Xiao
2021 Automated Software Engineering | November 2021
Project Snowflake: Non-blocking safe manual memory management in .NET
Matthew J. Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Manuel Costa, Pantazis Deligiannis, Aaron Blankstein, Dylan McDermott, Jonathan Balkind
MSR-TR-2017-32 | July 2017
Published by Microsoft
Starling: Lightweight Concurrency Verification with Views
Matt Windsor, Mike Dodds, Ben Simner, Matthew Parkinson
Computer Aided Verification 2017 | July 2017
Proving Linearizability Using Partial Orders (Extended Version)
Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson
July 2017
Simple, Fast and Safe Manual Memory Management
Piyus Kedia, Manuel Costa, Dimitrios Vytiniotis, Matthew J. Parkinson, Kapil Vaswani, Aaron Blankstein
Proceedings of the Conference on Programming Langauges Design and Implementation (PLDI) | June 2017
The F# Language Design RFCs (F# 4.0, 4.1)
Don Syme, Matthew J. Parkinson
May 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 Transactions on Programming Languages and Systems | May 2017, Vol 39(3)
A Generic Logic for Proving Linearizability
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
International Symposium on Formal Methods | November 2016
New Lace and Arsenic: adventures in weak memory with a program logic
Richard Bornat, Jade Alglave, Matthew J. Parkinson
November 2016
Matthew Parkinson
A Generic Logic for Proving Linearizability (Extended Version)
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
September 2016
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal
ACM Transactions on Programming Languages and Systems | January 2016, Vol 38(2)
The Push/Pull model of transactions
Eric Koskinen, Matthew J. Parkinson
ACM SIGPLAN Notices | June 2015, Vol 50(6): pp. 186-195
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
ECOOP 2013 - Object-Oriented Programming - 27th European Conference, Montpellier, France, July 1-5, 2013. Proceedings | August 2013
Separation Logic for Object-Oriented Programming
Matthew J. Parkinson, Gavin Bierman
Aliasing in Object-Oriented Programming. Types, Analysis and Verification | Published by Springer | 2013, Vol 7850 | Aliasing in Object-Oriented Programming. Types, Analysis and Verification edition
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
Christoph Haase, Samin Ishtiaq, Joel Ouaknine, Matthew J. Parkinson
Computer Aided Verification (CAV) | January 2013
Ribbon Proofs for Separation Logic
John Wickerson, Mike Dodds, Matthew J. Parkinson
Proceedings of ESOP | January 2013
Modular Reasoning about Separation for Concurrent Data Structures
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
Proceedings of ESOP | January 2013
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 | January 2011
Local Reasoning for Java
January 2005
January 2005
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-654.html
Separation logic and abstraction
Matthew J. Parkinson, Gavin Bierman
POPL '05 Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | January 2005
-
Concurrent Immediate Reference Counting
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang
PACM PL | June 2024
Coarse-grained transactions
Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | January 2010
ISBN: 978-1-60558-479-9
-
snmalloc: A message passing Allocator
David Chisnall, Sylvan Clebsch, Sophia Drossopoulou, Juliana Vicente Franco, Paul Lietar, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger
ISSM | June 2019, pp. 122-135
Proving Linearizability Using Partial Orders (Extended Version)
Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson
July 2017
Simple, Fast and Safe Manual Memory Management
Piyus Kedia, Manuel Costa, Dimitrios Vytiniotis, Matthew J. Parkinson, Kapil Vaswani, Aaron Blankstein
Proceedings of the Conference on Programming Langauges Design and Implementation (PLDI) | June 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 Transactions on Programming Languages and Systems | May 2017, Vol 39(3)
A Generic Logic for Proving Linearizability
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
International Symposium on Formal Methods | November 2016
New Lace and Arsenic: adventures in weak memory with a program logic
Richard Bornat, Jade Alglave, Matthew J. Parkinson
November 2016
Matthew Parkinson
A Generic Logic for Proving Linearizability (Extended Version)
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
September 2016
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal
ACM Transactions on Programming Languages and Systems | January 2016, Vol 38(2)
The Push/Pull model of transactions
Eric Koskinen, Matthew J. Parkinson
ACM SIGPLAN Notices | June 2015, Vol 50(6): pp. 186-195
-
Views: Compositional Reasoning for Concurrent Programs
Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang
Proceedings of POPL | January 2013
Uniqueness and Reference Immutability for Safe Parallelism
Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy
MSR-TR-2012-79 | October 2012
The Relationship Between Separation Logic and Implicit Dynamic Frames
Matthew J. Parkinson, Alexander J. Summers
Logical Methods in Computer Science | January 2012, Vol 8(3)
The Next 700 Separation Logics
2010 Verified Software: Theories, Tools, Experiments | August 2010
10.1007/978-3-642-15057-9_12
UpgradeJ: Incremental Typechecking for Class Upgrades
Gavin Bierman, Matthew J. Parkinson, James Noble
Proceedings of the 22nd European conference on Object-Oriented Programming | January 2008
ISBN: 978-3-540-70591-8
The java module system: core design and semantic definition
Rok Strniša, Peter Sewell, Matthew J. Parkinson
Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications | January 2007
ISBN: 978-1-59593-786-5
-
Proving that non-blocking algorithms don’t block
Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
SIGPLAN Notices | January 2009, Vol 44(1): pp. 16-28
Publications by Type
-
BatchIt: Optimizing Message-Passing Allocators for Producer-Consumer Workloads: An Intellectual Abstract
Nathaniel Filardo, Matthew J. Parkinson
Proceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management (ISMM'24) | June 2024
Reference Counting Deeply Immutable Data Structures with Cycles: an Intellectual Abstract
Matthew J. Parkinson, Sylvan Clebsch, Tobias Wrigstad
n Proceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management (ISMM ’24) | June 2024
Wait-Free Weak Reference Counting
Matthew J. Parkinson, Sylvan Clebsch, Ben Simner
ACM SIGPLAN International Symposium on Memory Management | June 2023
Nekara: Generalized Concurrency Testing
Udit Agarwal, Pantazis Deligiannis, Cheng Huang, Kumseok Jung, Akash Lal, Immad Naseer, Matthew J. Parkinson, Arun Thangamani, Jyothi Vedurada, Yunpeng Xiao
2021 Automated Software Engineering | November 2021
Starling: Lightweight Concurrency Verification with Views
Matt Windsor, Mike Dodds, Ben Simner, Matthew Parkinson
Computer Aided Verification 2017 | July 2017
Simple, Fast and Safe Manual Memory Management
Piyus Kedia, Manuel Costa, Dimitrios Vytiniotis, Matthew J. Parkinson, Kapil Vaswani, Aaron Blankstein
Proceedings of the Conference on Programming Langauges Design and Implementation (PLDI) | June 2017
A Generic Logic for Proving Linearizability
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
International Symposium on Formal Methods | November 2016
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
ECOOP 2013 - Object-Oriented Programming - 27th European Conference, Montpellier, France, July 1-5, 2013. Proceedings | August 2013
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
Christoph Haase, Samin Ishtiaq, Joel Ouaknine, Matthew J. Parkinson
Computer Aided Verification (CAV) | January 2013
Views: Compositional Reasoning for Concurrent Programs
Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang
Proceedings of POPL | January 2013
Ribbon Proofs for Separation Logic
John Wickerson, Mike Dodds, Matthew J. Parkinson
Proceedings of ESOP | January 2013
Modular Reasoning about Separation for Concurrent Data Structures
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
Proceedings of ESOP | January 2013
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 | January 2011
The Next 700 Separation Logics
2010 Verified Software: Theories, Tools, Experiments | August 2010
10.1007/978-3-642-15057-9_12
Coarse-grained transactions
Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | January 2010
ISBN: 978-1-60558-479-9
UpgradeJ: Incremental Typechecking for Class Upgrades
Gavin Bierman, Matthew J. Parkinson, James Noble
Proceedings of the 22nd European conference on Object-Oriented Programming | January 2008
ISBN: 978-3-540-70591-8
The java module system: core design and semantic definition
Rok Strniša, Peter Sewell, Matthew J. Parkinson
Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications | January 2007
ISBN: 978-1-59593-786-5
Separation logic and abstraction
Matthew J. Parkinson, Gavin Bierman
POPL '05 Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | January 2005
-
Concurrent Immediate Reference Counting
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang
PACM PL | June 2024
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, Vol 7(OOPSLA2)
Reference Capabilities for Flexible Memory Management
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, Matthew J. Parkinson, James Noble, Tobias Wrigstad
Proc. ACM Program. Lang. | October 2023, Vol 7(OOPSLA2)
snmalloc: A message passing Allocator
David Chisnall, Sylvan Clebsch, Sophia Drossopoulou, Juliana Vicente Franco, Paul Lietar, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger
ISSM | June 2019, pp. 122-135
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 Transactions on Programming Languages and Systems | May 2017, Vol 39(3)
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal
ACM Transactions on Programming Languages and Systems | January 2016, Vol 38(2)
The Push/Pull model of transactions
Eric Koskinen, Matthew J. Parkinson
ACM SIGPLAN Notices | June 2015, Vol 50(6): pp. 186-195
The Relationship Between Separation Logic and Implicit Dynamic Frames
Matthew J. Parkinson, Alexander J. Summers
Logical Methods in Computer Science | January 2012, Vol 8(3)
Proving that non-blocking algorithms don’t block
Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
SIGPLAN Notices | January 2009, Vol 44(1): pp. 16-28
-
Proving Linearizability Using Partial Orders (Extended Version)
Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson
July 2017
The F# Language Design RFCs (F# 4.0, 4.1)
Don Syme, Matthew J. Parkinson
May 2017
New Lace and Arsenic: adventures in weak memory with a program logic
Richard Bornat, Jade Alglave, Matthew J. Parkinson
November 2016
Matthew Parkinson
A Generic Logic for Proving Linearizability (Extended Version)
Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson
September 2016
-
Project Snowflake: Non-blocking safe manual memory management in .NET
Matthew J. Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Manuel Costa, Pantazis Deligiannis, Aaron Blankstein, Dylan McDermott, Jonathan Balkind
MSR-TR-2017-32 | July 2017
Published by Microsoft
Uniqueness and Reference Immutability for Safe Parallelism
Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy
MSR-TR-2012-79 | October 2012
-
Separation Logic for Object-Oriented Programming
Matthew J. Parkinson, Gavin Bierman
Aliasing in Object-Oriented Programming. Types, Analysis and Verification | Published by Springer | 2013, Vol 7850 | Aliasing in Object-Oriented Programming. Types, Analysis and Verification edition
-
Local Reasoning for Java
January 2005
January 2005
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-654.html