In Search of Compositional Verification for Concurrent Programs

From 2017 to 2018 was a Research Associate in Philippa Gardner's group at Imperial College London. From 2015 to 2017 I was a PostDoc in the Concurrency Theory Group at the University of Kaiserslautern, working with Prof. Roland Meyer.
In 2015 I received a PhD (DPhil) in Computer Science from the University of Oxford. My supervisor was Prof. C.-H. Luke Ong. My dissertation won the 2016 CPHC/BCS Distinguished Dissertation award.

I will focus on one of my latest projects, TaDA Live, a concurrent separation logics to reason compositionally about the termination of fine-grained concurrent programs. The Concurrent Separation Logics line of work achieved great compositionality for reasoning about partial correctness. We have comparatively little understanding of compositional reasoning about progress (liveness) properties: that is, something good eventually happens (e.g. termination, deadlock-freedom). Yet, the intricacies of the design of concurrent programs often arise precisely from the need to make the program correct with respect to progress properties.
In this talk, I will explain the design of TaDA Live total specifications and verification through examples. I will demonstrate that our specifications are expressive, concise, abstract, and can express atomicity. TaDA Live is joint work with J. Sutherland, A. Farzan and P. Gardner.