Matthew Parkinson

About

I am a Principal Researcher in the Confidential Computing group.  My research covers all aspects of memory safety including runtime implementations, programming language design, and verification.  My recent research focusses on Project Verona and its allocator snmalloc.  Project Verona is a new language to explore research about efficient and safe ways to manage memory.  It has a novel concurrency model, and we are developing a new type system to track ownership in a similar style to Pony.

My work on Separation Logic Verification for Java won the Dahl-Nygaard junior researcher prize in 2013 and the associated tool support, jStar won the OOPSLA 2008 most influential paper.  I was also very active in concurrency verification and developed many logics that combine ideas from separation logic with other concurrency verification techniques.

Prior to joining Microsoft in March 2010, I spent 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 did my Ph.D.  in Cambridge with on extending separation logic to reason about Java programs.