title:Many congratulations to Dr Julian Sutherland
---
We are very happy to announce (although a bit sad too) that Julian Sutherland, a long standing member of the group, has very successfully defended his PhD thesis today.
Many congratulations to Julian, and many thanks to [Derek Dreyer](https://www.mpg.de/18617632/software-systems-dreyer), [Joseph Tassarotti](http://www.cs.bc.edu/~tassarot/) and [Sophia Drossopoulou](https://wp.doc.ic.ac.uk/sd/), who acted as the examiners.
Julian’s thesis, Compositional termination verification for fine-grained concurrency, focuses on TaDA Live, a separation logic for proving liveness properties of concurrent programs. Liveness properties are concerned with showing that a program eventually reaches some desired state, in contrast to safety properties, which involve showing that a program never reaches a "bad/unsafe" state. Research work on proving liveness properties remains challenging and TaDA Live represents a substantial innovation, as it can handle reasoning about both non-blocking and blocking examples. TaDA Live can reason about the termination of clients which use abstract atomic operations that have blocking behaviour arising from busy-waiting patterns without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. The thesis also introduces a novel semantic model using layered subjective obligations to express liveness invariants, and a proof system that is sound with respect to the model.
Julian is currently a Formal Verification Engineer at [Nethermind](https://nethermind.io/), a blockchain company working on Ethereum.
