| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 9656090 | Electronic Notes in Theoretical Computer Science | 2005 | 17 Pages |
Abstract
The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated pGCL program and its partial correctness specification, and derives from that a sufficient set of verification conditions. This is employed to verify the partial correctness of the probabilistic voting stage in Rabin's mutual-exclusion algorithm [Eyal Kushilevitz and Michael O. Rabin. Randomized mutual exclusion algorithms revisited. In Maurice Herlihy, editor, Proceedings of the 11th Annual Symposium on Principles of Distributed Computing, pages 275-283, Vancouver, BC, Canada, August 1992. ACM Press].
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Joe Hurd, Annabelle McIver, Carroll Morgan,