Probabilistic guarded commands mechanized in HOL
<p>The probabilistic guarded-command language (<em>pGCL</em>) 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- (...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Elsevier
2005
|
| Subjects: |
| _version_ | 1797079698067423232 |
|---|---|
| author | Hurd, J McIver, A Morgan, C |
| author_facet | Hurd, J McIver, A Morgan, C |
| author_sort | Hurd, J |
| collection | OXFORD |
| description | <p>The probabilistic guarded-command language (<em>pGCL</em>) 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.</p> <p>We present a mechanization of the quantitative logic for <em>pGCL</em>using the <em>HOL</em> theorem prover, including a proof that all <em>pGCL</em>commands satisfy the new condition <em>sublinearity</em>, the quantitative generalization of <em>conjunctivity</em> for standard <em>GCL</em>.</p> <p>The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated <em>pGCL</em>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 <em>mutual-exclusion</em> algorithm.</p> |
| first_indexed | 2024-03-07T00:49:28Z |
| format | Journal article |
| id | oxford-uuid:85e3a354-dd4d-49f3-9f21-c9e03a0565f9 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T00:49:28Z |
| publishDate | 2005 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:85e3a354-dd4d-49f3-9f21-c9e03a0565f92022-03-26T22:00:26ZProbabilistic guarded commands mechanized in HOLJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:85e3a354-dd4d-49f3-9f21-c9e03a0565f9Theory and automated verificationEnglishOxford University Research Archive - ValetElsevier2005Hurd, JMcIver, AMorgan, C<p>The probabilistic guarded-command language (<em>pGCL</em>) 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.</p> <p>We present a mechanization of the quantitative logic for <em>pGCL</em>using the <em>HOL</em> theorem prover, including a proof that all <em>pGCL</em>commands satisfy the new condition <em>sublinearity</em>, the quantitative generalization of <em>conjunctivity</em> for standard <em>GCL</em>.</p> <p>The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated <em>pGCL</em>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 <em>mutual-exclusion</em> algorithm.</p> |
| spellingShingle | Theory and automated verification Hurd, J McIver, A Morgan, C Probabilistic guarded commands mechanized in HOL |
| title | Probabilistic guarded commands mechanized in HOL |
| title_full | Probabilistic guarded commands mechanized in HOL |
| title_fullStr | Probabilistic guarded commands mechanized in HOL |
| title_full_unstemmed | Probabilistic guarded commands mechanized in HOL |
| title_short | Probabilistic guarded commands mechanized in HOL |
| title_sort | probabilistic guarded commands mechanized in hol |
| topic | Theory and automated verification |
| work_keys_str_mv | AT hurdj probabilisticguardedcommandsmechanizedinhol AT mcivera probabilisticguardedcommandsmechanizedinhol AT morganc probabilisticguardedcommandsmechanizedinhol |