Verifying a Self-Stabilizing Mutual Exclusion Algorithm
- Natarajan Shankar ,
- Shaz Qadeer
Working Conference on Programming Concepts and Methods (PROCOMET '98) |
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.