About
I am a Researcher in the Programming Principles and Tools group. I am investigating memory management for managed programming languages. I am also working on verification for concurrent programs.
Prior to joining Microsoft in March 2010, I spent the last four years in the Cambridge Computer Lab on an RAEng/EPSRC research fellowship investigating how to verify object-oriented and concurrent programs meet their specifications. I have also made some brief forays into programming language semantics and design.
Before the research fellowship I did a post-doc with Richard Bornat verifying crazy concurrent programs running on exotic hardware. And prior to that I did a Ph.D. in the Computer Lab in Cambridge with Gavin Bierman and Andrew Pitts on extending separation logic to reason about Java programs.
Publications
2013
Separation Logic for Object-Oriented Programming
Matthew Parkinson, Gavin Bierman, in Aliasing in Object-Oriented Programming. Types, Analysis and Verification, Springer, May 1, 2013, View abstract, View external linkModular Reasoning about Separation for Concurrent Data Structures
Kasper Svendsen, Lars Birkedal, Matthew Parkinson, in Proceedings of ESOP, January 1, 2013, View abstract, Download PDFRibbon Proofs for Separation Logic
John Wickerson, Mike Dodds, Matthew Parkinson, in Proceedings of ESOP, January 1, 2013, View abstract, Download PDFSeLoger: A Tool for Graph-Based Reasoning in Separation Logic
Christoph Haase, Samin Ishtiaq, Joel Ouaknine, Matthew Parkinson, in Computer Aided Verification (CAV), January 1, 2013, View abstract, Download PDFViews: Compositional Reasoning for Concurrent Programs
Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, Hongseok Yang, in Proceedings of POPL, January 1, 2013, View abstract, Download PDF2012
Uniqueness and Reference Immutability for Safe Parallelism
Colin S. Gordon, Matthew Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy, Microsoft Research, October 1, 2012, View abstract, Download PDFUniqueness and reference immutability for safe parallelism
Colin S. Gordon, Matthew Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy, in OOPSLA, October 1, 2012, View abstractThe Relationship Between Separation Logic and Implicit Dynamic Frames
Matthew Parkinson, Alexander J. Summers, in Logical Methods in Computer Science, January 1, 2012, View abstract, View external link2011
Automatic safety proofs for asynchronous memory operations
, Mike Dodds, Alastair F. Donaldson, Matthew Parkinson, in PPOPP, January 1, 2011, View abstractjStar-eclipse: an IDE for automated verification of Java programs
Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Matthew Parkinson, , in SIGSOFT FSE, January 1, 2011, View abstract, Download PDFModular reasoning for deterministic parallelism
Mike Dodds, Suresh Jagannathan, Matthew Parkinson, in POPL, January 1, 2011, View abstractSafe asynchronous multicore memory operations
, Mike Dodds, Alastair F. Donaldson, Matthew Parkinson, in ASE, January 1, 2011, View abstractThe Relationship between Separation Logic and Implicit Dynamic Frames
Matthew Parkinson, Alexander J. Summers, in ESOP, January 1, 2011, View abstract2010
The Next 700 Separation Logics
Matthew Parkinson, in Verified Software: Theories, Tools, Experiments, Springer Berlin / Heidelberg, August 1, 2010, View abstract, View external linkConcurrent Abstract Predicates
Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, Viktor Vafeiadis, in ECOOP, Springer Verlag, June 1, 2010, View abstractVerifying Generics and Delegates
Kasper Svendsen, Lars Birkedal, Matthew Parkinson, in Proceedings of ECOOP, June 1, 2010, View abstractCoarse-grained transactions
Eric Koskinen, Matthew Parkinson, Maurice Herlihy, in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, January 1, 2010, View abstract, View external linkExplicit Stabilisation for Modular Rely-Guarantee Reasoning
John Wickerson, Mike Dodds, Matthew Parkinson, in ESOP, January 1, 2010, View abstract2009
Deny-Guarantee Reasoning
Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis, in ESOP, Springer Verlag, January 1, 2009, View abstractProving that non-blocking algorithms don’t block
Alexey Gotsman, Byron Cook, Matthew Parkinson, Viktor Vafeiadis, in SIGPLAN Notices, ACM, January 1, 2009, View abstract, View external linkSeparation Logic Verification of C Programs with an SMT Solver
, Matthew Parkinson, Wolfram Schulte, in Electr. Notes Theor. Comput. Sci., January 1, 2009, View abstract2008
jStar: towards practical verification for java
Dino Distefano, Matthew Parkinson, in OOPSLA, Association for Computing Machinery, Inc., January 1, 2008, View abstractSeparation Logic, Abstraction and Inheritance
Matthew Parkinson, Gavin Bierman, in ACM Symposium on Principles of Programming Languages (POPL'08), Association for Computing Machinery, Inc., January 1, 2008, View abstractUpgradeJ: Incremental Typechecking for Class Upgrades
Gavin Bierman, Matthew Parkinson, James Noble, in Proceedings of the 22nd European conference on Object-Oriented Programming, Springer-Verlag, January 1, 2008, View abstract, View external link2007
A marriage of Rely/Guarantee and Separation Logic
Viktor Vafeiadis, Matthew Parkinson, in CONCUR, Springer Verlag, January 1, 2007, View abstractModular Safety Checking for Fine-Grained Concurrency
Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis, in SAS, Springer Verlag, January 1, 2007, View abstractModular Verification of a Non-Blocking Stack
Matthew Parkinson, Richard Bornat, Peter O'Hearn, in POPL, Association for Computing Machinery, Inc., January 1, 2007, View abstractThe java module system: core design and semantic definition
Rok Strniša, Peter Sewell, Matthew Parkinson, in Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, ACM, January 1, 2007, View abstract, View external link2006
Variables as resource in Hoare Logic
Matthew Parkinson, Richard Bornat, Cristiano Calcagno, in Proceedings of LICS, IEEE, January 1, 2006, View abstract2005
Permission accounting in separation logic
Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew Parkinson, in POPL, January 1, 2005, View abstractSeparation logic and abstraction
Matthew Parkinson, Gavin Bierman, in POPL '05 Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 1, 2005, View abstract, View external linkProjects
Link description
A Marriage of Rely/Guarantee and Separation Logic
Date
June 30, 2008
Speakers
Matthew Parkinson
Affiliation
University of Cambridge
Link description
When Separation Logic met Java
Date
August 9, 2006
Speakers
Matthew Parkinson
Affiliation
University of Cambridge