Probabilistic guarded commands mechanized in HOL

DOI10.1016/j.tcs.2005.08.005zbMath1080.68063OpenAlexW2113081700MaRDI QIDQ2576950

Carroll Morgan, Joe Hurd, Annabelle McIver

Publication date: 29 December 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:85e3a354-dd4d-49f3-9f21-c9e03a0565f9

zbMATH Keywords

formal verificationprobabilistic programspGCL

Mathematics Subject Classification ID

Related Items (13)

Understanding Probabilistic Programs ⋮ Model Checking Probabilistic Systems ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ A game-based abstraction-refinement framework for Markov decision processes ⋮ Formalizing Probabilistic Noninterference ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Automated reasoning for probabilistic sequential programs with theorem proving ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Proofs of randomized algorithms in Coq ⋮ Using probabilistic Kleene algebra pKA for protocol verification ⋮ Three Chapters of Measure Theory in Isabelle/HOL ⋮ Formalising Semantics for Expected Running Time of Probabilistic Programs ⋮ Using theorem proving to verify expectation and variance for discrete random variables

Uses Software

• PRISM
• ML
• HOL
• pGCL

Cites Work

• A probabilistic PDL
• Edinburgh LCF. A mechanized logic of computation
• Programming as a Discipline of Mathematical Nature
• Randomized mutual exclusion algorithms revisited
• Partial correctness for probabilistic demonic programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Probabilistic guarded commands mechanized in HOL