Partial correctness for probabilistic demonic programs

DOI10.1016/S0304-3975(00)00208-5zbMath0992.68137MaRDI QIDQ5958768

Carroll Morgan, Annabelle McIver

Publication date: 3 March 2002

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

zbMATH Keywords

verificationprobabilitypartial correctnessprogram logic

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items (17)

A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Denotational Semantics for a Probabilistic Timed Shared-Variable Language ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Model Checking Temporal Properties of Recursive Probabilistic Programs ⋮ Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language ⋮ Data Refinement with Probability in Mind ⋮ Proof rules for the correctness of quantum programs ⋮ Topological cones: functional analysis in a \(T_{0}\)-setting ⋮ Semantics of non-deterministic possibility computation ⋮ Compiling quantum programs ⋮ Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language ⋮ Partial correctness for probabilistic demonic programs ⋮ Semi-decidability of May, Must and Probabilistic Testing in a Higher-type Setting ⋮ Predicate transformers for extended probability and non-determinism ⋮ A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language ⋮ Probabilistic guarded commands mechanized in HOL ⋮ Remarks on Testing Probabilistic Processes

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unifying wp and wlp
• Domain theory and integration
• A probabilistic dynamic logic
• Semantics of probabilistic programs
• The generalized Riemann integral on locally compact spaces
• PCF extended with real numbers
• Probabilistic models for the guarded command language
• Programs, Recursion and Unbounded Choice
• Programming as a Discipline of Mathematical Nature
• Demonic, angelic and unbounded probabilistic choices in sequential programs
• Partial correctness for probabilistic demonic programs

This page was built for publication: Partial correctness for probabilistic demonic programs