Probabilistic guarded commands mechanized in HOL

Journal article

The probabilistic guarded-command language (pGCL) contains both demonic and probabilistic non-determinism, 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 pGCLusing the HOL theorem prover, including a proof that all pGCLcommands 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 pGCLprogram 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.

Authors: Hurd, J; McIver, A; Morgan, C

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Theoretical Computer Science
• Volume: 346
• Issue: 1
• Pages: 96–112
• Publication date: 2005-11-01
• Edition: Publisher's version
• DOI: 10.1016/j.tcs.2005.08.005
• ISSN: 0304-3975
• Language: English
• Keywords: formal verification; probabilistic programs; pGCL
• Subjects: Theory and automated verification