TY - JOUR

T1 - Probabilistic Guarded Commands Mechanized in HOL

AU - Hurd, Joe

AU - McIver, Annabelle

AU - Morgan, Carroll

PY - 2005/1/2

Y1 - 2005/1/2

N2 - 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.

AB - 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.

KW - Formal verification

KW - pGCL

KW - Probabilistic programs

UR - http://www.scopus.com/inward/record.url?scp=11344271122&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2004.01.021

DO - 10.1016/j.entcs.2004.01.021

M3 - Article

AN - SCOPUS:11344271122

SN - 1571-0661

VL - 112

SP - 95

EP - 111

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - SPEC. ISS.

ER -