SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Verifying a Self-Stabilizing Mutual Exclusion Algorithm
 by Dr. Natarajan Shankar & Shaz Qadeer.

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.


Abstract
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.
BibTEX Entry
@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/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy