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.
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.