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