Matthew Parkinson
Principal Researcher
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 (opens in new tab) and its allocator snmalloc (opens in new tab). 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 (opens in new tab) and the associated tool support, jStar won the OOPSLA 2008 most influential paper (opens in new tab). I was also very active in concurrency verification and developed many logics that combine ideas from separation logic with other concurrency verification techniques. The Views paper that combines many of these ideas won the POPL 2013 most influential paper (opens in new tab).
Prior to joining Microsoft in March 2010, I spent four years in the Cambridge Computer Lab (opens in new tab)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 (opens in new tab)on extending separation logic to reason about Java programs.