On the Verification of a Self-Stabilizing Algorithm

Stephan Merz
This note documents an Isabelle verification of one of Dijkstra's self-stabilizing protocols. It was inspired by a paper by Qadeer and Shankar and improves on their proof. Although the Isabelle proof is entirely conventional, the final section shows a diagrammatic representation of the main proof idea and observes that the proof could be significantly simplified by giving the diagram a formal status and performing model checking on the finite diagram. This idea was further developed into the notion of predicate diagrams.
Available as:  gzip'ed Postscript 
  author = {Stephan Merz},
  title =  {On the verification of a self-stabilizing algorithm},
  note =   {Available at
  year =   {1998}

Stephan Merz