We are very, very happy to announce 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, Joseph Tassarotti and Sophia Drossopoulou, 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, a blockchain company working on Ethereum.