Matthew Parkinson
RESEARCHER
.
I am a Researcher in the Programming Principles and Tools group. I am investigating different ways to verify concurrent programs, and decision procedures for separation logic.
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
- Christoph Haase, Samin Ishtiaq, Joel Ouaknine, and Matthew Parkinson, SeLoger: A Tool for Graph-Based Reasoning in Separation Logic , in Computer Aided Verification (CAV), 2013
- Kasper Svendsen, Lars Birkedal, and Matthew Parkinson, Modular Reasoning about Separation for Concurrent Data Structures, in Proceedings of ESOP, 2013
- John Wickerson, Mike Dodds, and Matthew Parkinson, Ribbon Proofs for Separation Logic, in Proceedings of ESOP, 2013
- Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang, Views: Compositional Reasoning for Concurrent Programs, in Proceedings of POPL, 2013
2012
- Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy, Uniqueness and Reference Immutability for Safe Parallelism, no. MSR-TR-2012-79, October 2012
- Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy, Uniqueness and reference immutability for safe parallelism, in OOPSLA, October 2012
- John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew J. Parkinson, Behavioral interface specification languages, in ACM Comput. Surv., vol. 44, no. 3, pp. 16, 2012
- Matthew J. Parkinson and Alexander J. Summers, The Relationship Between Separation Logic and Implicit Dynamic Frames, in Logical Methods in Computer Science, vol. 8, no. 3, 2012
2011
- Mike Dodds, Suresh Jagannathan, and Matthew J. Parkinson, Modular reasoning for deterministic parallelism, in POPL, 2011
- Matko Botincan, Mike Dodds, Alastair F. Donaldson, and Matthew J. Parkinson, Safe asynchronous multicore memory operations, in ASE, 2011
- Matthew J. Parkinson and Alexander J. Summers, The Relationship between Separation Logic and Implicit Dynamic Frames, in ESOP, 2011
- Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, and Matthew J. Parkinson, jStar-eclipse: an IDE for automated verification of Java programs, in SIGSOFT FSE, 2011
- Matko Botincan, Mike Dodds, Alastair F. Donaldson, and Matthew J. Parkinson, Automatic safety proofs for asynchronous memory operations, in PPOPP, 2011
2010
- Matthew J. Parkinson, The Next 700 Separation Logics, in Verified Software: Theories, Tools, Experiments, Springer Berlin / Heidelberg, August 2010
- Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis, Concurrent Abstract Predicates, in ECOOP, Springer Verlag, June 2010
- Kasper Svendsen, Lars Birkedal, and Matthew Parkinson, Verifying Generics and Delegates, in Proceedings of ECOOP, June 2010
- Eric Koskinen, Matthew Parkinson, and Maurice Herlihy, Coarse-grained transactions, in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, New York, NY, USA, 2010
- John Wickerson, Mike Dodds, and Matthew J. Parkinson, Explicit Stabilisation for Modular Rely-Guarantee Reasoning, in ESOP, 2010
2009
- Matko Botincan, Matthew J. Parkinson, and Wolfram Schulte, Separation Logic Verification of C Programs with an SMT Solver, in Electr. Notes Theor. Comput. Sci., vol. 254, pp. 5-23, 2009
- Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis, Proving that non-blocking algorithms don't block, in SIGPLAN Not., vol. 44, pp. 16–28, ACM, New York, NY, USA, January 2009
- Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis, Deny-Guarantee Reasoning, in ESOP, Springer Verlag, 2009
2008
- Dino Distefano and Matthew J. Parkinson, jStar: towards practical verification for java, in OOPSLA, Association for Computing Machinery, Inc., 2008
- Gavin Bierman, Matthew Parkinson, and James Noble, UpgradeJ: Incremental Typechecking for Class Upgrades, in Proceedings of the 22nd European conference on Object-Oriented Programming, Springer-Verlag, Berlin, Heidelberg, 2008
- Matthew Parkinson and Gavin Bierman, Separation Logic, Abstraction and Inheritance, in ACM Symposium on Principles of Programming Languages (POPL'08), Association for Computing Machinery, Inc., January 2008
2007
- Viktor Vafeiadis and Matthew J. Parkinson, A marriage of Rely/Guarantee and Separation Logic, in CONCUR, Springer Verlag, 2007
- Rok Strniša, Peter Sewell, and Matthew Parkinson, The java module system: core design and semantic definition, in Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, ACM, New York, NY, USA, 2007
- Cristiano Calcagno, Matthew J. Parkinson, and Viktor Vafeiadis, Modular Safety Checking for Fine-Grained Concurrency, in SAS, Springer Verlag, 2007
- Matthew J. Parkinson, Richard Bornat, and Peter O'Hearn, Modular Verification of a Non-Blocking Stack, in POPL, Association for Computing Machinery, Inc., January 2007
2006
- Matthew J. Parkinson, Richard Bornat, and Cristiano Calcagno, Variables as resource in Hoare Logic, in Proceedings of LICS, IEEE, 2006
2005
- Matthew J. Parkinson and Gavin M. Bierman, Separation logic and abstraction, in POPL, 2005
- Matthew J. Parkinson, Local Reasoning for Java, 2005
- Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, and Matthew J. Parkinson, Permission accounting in separation logic, in POPL, 2005
