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