### On the Verification of a Self-Stabilizing Algorithm

Stephan Merz
Contents
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
Reference
```@Unpublished{merz:self-stabilizing,
author = {Stephan Merz},
title =  {On the verification of a self-stabilizing algorithm},
note =   {Available at
\url{http://www.loria.fr/~merz/papers/dijkstra.ps.gz}},
year =   {1998}
}
```

Stephan Merz