article

Probabilistic guarded commands mechanized in HOL

Authors:

Annabelle McIver,

Carroll MorganAuthors Info & Claims

Theoretical Computer Science, Volume 346, Issue 1

Pages 96 - 112

https://doi.org/10.1016/j.tcs.2005.08.005

Published: 23 November 2005 Publication History

Abstract

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

References

[1]

{1} E.W. Dijkstra, A Discipline of Programming, Prentice-Hall, Englewood Cliffs, NJ, 1976.]]

Digital Library

[2]

{2} M.J.C. Gordon, Mechanizing programming logics in higher order logic, in: G. Birtwistle, P.A. Subrahmanyam (Eds.), Current Trends in Hardware Verification and Automated Theorem Proving, Springer, Berlin, 1989, pp. 387-439.]]

Digital Library

[3]

{3} M.J.C. Gordon, T.F. Melham, Introduction to HOL (A theorem-proving environment for higher order logic), Cambridge University Press, Cambridge, 1993.]]

Digital Library

[4]

{4} M. Gordon, R. Milner, C. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science, Vol. 78, Springer, Berlin, 1979.]]

[5]

{5} J. Harrison, Formalizing Dijkstra, in: J. Grundy, M. Newey (Eds.), Theorem Proving in Higher Order Logics, 11th Internat. Conf., TPHOLs '98, Lecture Notes in Computer Science, Vol. 1497, Canberra, Australia, Springer, Berlin, September 1998, pp. 171-188.]]

Digital Library

[6]

{6} T.S. Hoang, Z. Jin, K. Robinsion, A.K. McIver, C.C. Morgan, Probabilistic invariants for probabilistic machines, in: Proc. third Internat. Conf. of B and Z Users 2003, Lecture Notes in Computer Science, Vol. 2651, Springer, Berlin, pp. 240-159.]]

[7]

{7} J. Hurd, Formal verification of probabilistic algorithms, Ph.D. Thesis, University of Cambridge, 2002.]]

[8]

{8} M. Huth, The interval domain: a matchmaker for aCTL and aPCTL, in: R. Cleaveland, M. Mislove, P. Mulry (Eds.), US-Brazil Joint Workshops on the Formal Foundations of Software Systems, Electronic Notes in Theoretical Computer Science, Vol. 14, Elsevier, Amsterdam, 2000.]]

[9]

{9} D. Kozen. A probabilistic PDL, Proc. 15th ACM Symp. on Theory of Computing, 1983.]]

Digital Library

[10]

{10} E. Kushilevitz, M.O. Rabin, Randomized mutual exclusion algorithms revisited, in: M. Herlihy (Ed.), Proc. 11th Ann. Symp. on Principles of Distributed Computing, Vancouver, BC, Canada, ACM Press, New york, August 1992, pp. 275-283.]]

Digital Library

[11]

{11} M. Kwiatkowska, G. Norman, D. Parker, Prism: probabilistic symbolic model checker, in: Proc. of PAPM/PROBMIV 2001 Tools Session, September 2001.]]

[12]

{12} A.K. McIver, C.C. Morgan, Partial correctness for probabilistic programs, Theoret. Comput. Sci. 266 (1-2) (2001) 513-541.]]

Digital Library

[13]

{14} C. Morgan, Proof rules for probabilistic loops, in: H. Jifeng, J. Cooke, P. Wallis (Eds.), Proc. BCS-FACS 7th Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996.]]

[14]

{15} C. Morgan, A. McIver, pGCL: formal reasoning for random algorithms, South African Comput. J. 22 (1999) 14-27.]]

[15]

{16} C. Morgan, A. McIver, K. Seidel, Probabilistic predicate transformers, ACM Trans. Programming Languages Systems 18 (3) (1996) 325-353 See also {12}.]]

Digital Library

[16]

{17} T. Nipkow, Hoare logics in Isabelle/HOL, in: H. Schwichtenberg, R. Steinbrüggen (Eds.), Proof and System-Reliability, Kluwer, Dordrecht, 2002, pp. 341-367.]]

Digital Library

[17]

{18} J. Shield, I.J. Hayes, D.A. Carrington, Using theory interpretation to mechanise the reals in a theorem prover, in: C. Fidge (Ed.), Electronic Notes in Theoretical Computer Science, Vol. 42, Elsevier, Amsterdam, 2001.]]

Cited By

Schröer PBatz KKaminski BKatoen JMatheja C(2023)A Deductive Verification Infrastructure for Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36228707:OOPSLA2(2052-2082)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622870
Hirata MMinamide YSato T(2023)Program logic for higher-order probabilistic programs in Isabelle/HOLScience of Computer Programming10.1016/j.scico.2023.102993230:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.scico.2023.102993
Navarro MOlmedo F(2022)Slicing of probabilistic programs based on specificationsScience of Computer Programming10.1016/j.scico.2022.102822220:COnline publication date: 1-Aug-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102822
Show More Cited By

Recommendations

Probabilistic Guarded Commands Mechanized in HOL

The probabilistic guarded-command language pGCL Carroll Morgan, Annabelle McIver. pGCL: formal reasoning for random algorithms. South African Computer Journal (1999)] contains both demonic and probabilistic nondeterminism, which makes it suitable for ...
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs

We present quantitative separation logic (QSL). In contrast to classical separation logic, QSL employs quantities which evaluate to real numbers instead of predicates which evaluate to Boolean values. The connectives of classical separation logic, ...
Program logic for higher-order probabilistic programs in Isabelle/HOL
Abstract
The verification framework PPV (Probabilistic Program Verification) verifies functional probabilistic programs supporting higher-order functions, continuous distributions, and conditional inference. PPV is based on the theory of quasi-Borel ...
Highlights
- We formalize quasi-Borel spaces in Isabelle/HOL.
- We formalize the probability monad on the category of quasi-Borel spaces.
- We formalize the system PPV in Isabelle/HOL.
- We verify the Monte Carlo approximation in our mechanized ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 346, Issue 1

Quantitative aspects of programming languages (QAPL 2004)

23 November 2005

182 pages

ISSN:0304-3975

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 23 November 2005

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Schröer PBatz KKaminski BKatoen JMatheja C(2023)A Deductive Verification Infrastructure for Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36228707:OOPSLA2(2052-2082)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622870
Hirata MMinamide YSato T(2023)Program logic for higher-order probabilistic programs in Isabelle/HOLScience of Computer Programming10.1016/j.scico.2023.102993230:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.scico.2023.102993
Navarro MOlmedo F(2022)Slicing of probabilistic programs based on specificationsScience of Computer Programming10.1016/j.scico.2022.102822220:COnline publication date: 1-Aug-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102822
Ye KFoster SWoodcock J(2021)Automated Reasoning for Probabilistic Sequential Programs with Theorem ProvingRelational and Algebraic Methods in Computer Science10.1007/978-3-030-88701-8_28(465-482)Online publication date: 2-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-88701-8_28
Sato TAguirre ABarthe GGaboardi MGarg DHsu J(2019)Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimizationProceedings of the ACM on Programming Languages10.1145/32903513:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290351
Olmedo FGretz FJansen NKaminski BKatoen JMciver A(2018)Conditioning in Probabilistic ProgrammingACM Transactions on Programming Languages and Systems10.1145/315601840:1(1-50)Online publication date: 3-Jan-2018
https://dl.acm.org/doi/10.1145/3156018
Hölzl JBertot YVafeiadis V(2017)Markov processes in Isabelle/HOLProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs10.1145/3018610.3018628(100-111)Online publication date: 16-Jan-2017
https://dl.acm.org/doi/10.1145/3018610.3018628
Hölzl J(2017)Markov Chains and Markov Decision Processes in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-016-9401-559:3(345-387)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10817-016-9401-5
Rand RZdancewic S(2015)VPHLElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2015.12.021319:C(351-367)Online publication date: 21-Dec-2015
https://dl.acm.org/doi/10.1016/j.entcs.2015.12.021
Barthe GFournet CGrégoire BStrub PSwamy NZanella-Béguelin S(2014)Probabilistic relational verification for cryptographic implementationsACM SIGPLAN Notices10.1145/2578855.253584749:1(193-205)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535847
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents