Probabilistic Guarded Commands Mechanized in HOL

Joe Hurd, Annabelle McIver, Carroll Morgan

Research output: Contribution to journalArticle

9 Citations (Scopus)

Abstract

The probabilistic guarded-command language pGCL contains both demonic and probabilistic nondeterminism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based on weakest precondition semantics, using an underlying logic of real- (rather than Boolean-) valued functions. We present a mechanization of the quantitative logic for pGCL using the HOL theorem prover, including a proof that all pGCL commands satisfy the new condition sublinearity, the quantitative generalization of conjunctivity for standard GCL. 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.

Original languageEnglish
Pages (from-to)95-111
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Volume112
Issue numberSPEC. ISS.
DOIs
Publication statusPublished - 2 Jan 2005

Keywords

  • Formal verification
  • pGCL
  • Probabilistic programs

Fingerprint Dive into the research topics of 'Probabilistic Guarded Commands Mechanized in HOL'. Together they form a unique fingerprint.

Cite this