| #
8186796c |
|
08-Apr-2003 |
Joe Hurd <joe@gilith.com> |
A HOL example formalizing pGCL (Probabilistic Guarded Command Language).
pGCL supports both demonic and probabilistic choice, so can in principle
be applied to the verification of distributed random algorithms.
The high-point of this example is the verification of the probabilistic
voting scheme in Rabin's mutual exclusion algorithm.
|