In previous work, we have verified safety properties of mutual exclusion algorithms with safe and regular registers.
At the time, liveness verification was hindered by the existence of unrealistic counterexamples.
In recently published work, we have presented modal mu-calculus formulae that allow us to check liveness properties under a variety of completeness criteria such as justness and weak fairness.
Using these formulae, we can now verify liveness while ignoring those unrealistic counterexamples
In this presentation, I will present some preliminary results on liveness of Dekker’s mutual exclusion algorithm with safe registers.

This presentation includes joint work with Bas Luttik and Tim Willemse.