CS Talk
January 30, 2012
4:00 p.m., AKW 200

Host: Zhong Shao

Speaker: Matthew Parkinson, Microsoft Research Cambridge
Title: The Next 700 Separation Logics

Abstract: In recent years, separation logic has brought great advances in the world of verification. However, there is a disturbing trend for each new library or concurrency primitive to require a new separation logic. I will argue that we shouldn’t be inventing new separation logics, but should find the right logic to reason about interference, and have a powerful abstraction mechanism to enable the library’s implementation details to be correctly abstracted. Adding new concurrency libraries should simply be a matter of verification, not of new logics or metatheory.

Bio: Matthew Parkinson is a Researcher at Microsoft Research Cambridge. He is working on software verification for concurrent programs. Prior to joining Microsoft, he 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. Before the research fellowship he did a post-doc with Richard Bornat verifying crazy concurrent programs running on exotic hardware. Prior to that he was a Ph.D. student in the Computer Lab at the University of Cambridge working with Gavin Bierman on extending separation logic to reason about Java programs.