From IFIP Working Conference on Programming Concepts and Methods (PROCOMET '98).
Edited by David Gries and Willem-Paul de Roever.
Chapman & Hall, Shelter Island, NY.
June, 1998.
Pages 424–443.

We present a detailed description of a machine-assisted verification of an algorithm for self-stabilizing mutual exclusion that is due to Dijkstra. This verification was constructed using PVS. We compare the mechanical verification to the informal proof sketch on which it is based. This comparison yields several observations regarding the challenges of formalizing and mechanically verifying distributed algorithms in general.

@inproceedings{Qadeer&Shankar98,
    AUTHOR = {Shaz Qadeer and Natarajan Shankar},
    TITLE = {Verifying a Self-Stabilizing Mutual Exclusion Algorithm},
    BOOKTITLE = {{IFIP} Working Conference on Programming Concepts and Methods (PROCOMET '98)},
    YEAR = {1998},
    EDITOR = {David Gries and Willem-Paul de Roever},
    PAGES = {424--443},
    ADDRESS = {Shelter Island, {NY}},
    MONTH = {jun},
    PUBLISHER = {Chapman \& Hall},
    URL = {http://www.csl.sri.com/papers/stable-paper/}
}

• stable-paper.ps.gz