Probabilistic guarded commands mechanized in HOL - Hurd, J; McIver, A; Morgan, C (Theoretical Computer Science, 2005)