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

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