Campus Event Calendar

Event Entry

What and Who

In Search of Compositional Verification for Concurrent Programs

Emanuele D'Osualdo
Imperial College London
Colloquium Lecture

Emanuele D'Osualdo is a Marie-Curie Fellow at Imperial College London, working on verification of concurrent software with Prof. P. Gardner.

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.

AG 3, SWS, RG1, MMCI  
AG Audience

Date, Time and Location

Wednesday, 20 May 2020
60 Minutes
E1 5


In this talk, I will give a brief overview of my research so far, in search of scalable verification for concurrent software.

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.


Danielle Dalton
+49 681 9303 9106
--email hidden

Danielle Dalton, 05/19/2020 12:10 PM -- Created document.