language: en

Verifying a Self-Stabilizing Mutual Exclusion Algorithm

[To Appear in the Proceedings of PROCOMET'98]

Shaz Qadeer
Department of EECS University of California at Berkeley
Berkeley CA 94720

[Phone: (510)642-1490]

shaz@eecs.berkeley.edu
Natarajan Shankar
Computer Science Laboratory SRI International
Menlo Park CA 94025

[Phone: (415)859-5272]

shankar@csl.sri.com

Abstract We present a detailed description of a machine-assisted verification of an algorithm for self-stabilizing mutual exclusion that is due to Dijkstra [Dij74]. 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.

1 Introduction