Abstraction, Refinement and Proof for Probabilistic Systems
From MaRDI portal
Publication:4650346
DOI10.1007/b138392zbMath1069.68039OpenAlexW1734364899MaRDI QIDQ4650346
Carroll Morgan, Annabelle McIver
Publication date: 11 February 2005
Published in: Monographs in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b138392
Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Randomized algorithms (68W20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Formal semantics of a classical-quantum language ⋮ Modelling web-service uncertainty: the angel/daemon approach ⋮ Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting ⋮ Algebra for Quantitative Information Flow ⋮ A UTP approach for rTiMo ⋮ Learning probabilistic termination proofs ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ Quantitative logics for equivalence of effectful programs ⋮ A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Weakest preconditions in fibrations ⋮ ``Keep definition, change category -- a practical approach to state-based system calculi ⋮ Understanding Probabilistic Programs ⋮ Tank monitoring: A pAMN case study ⋮ Testing Finitary Probabilistic Processes ⋮ Typed Linear Algebra for Weigthed (Probabilistic) Automata ⋮ Out of control: reducing probabilistic models by control-state elimination ⋮ A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems ⋮ Formalizing Probabilistic Noninterference ⋮ The computational complexity of QoS measures for orchestrations. The computational complexity of QoS measures ⋮ Approximate counting in SMT and value estimation for probabilistic programs ⋮ A debugger for probabilistic programs ⋮ Relations into algebras of probabilistic distributions ⋮ A specification logic for programs in the probabilistic guarded command language ⋮ Program algebra for quantitative information flow ⋮ Towards a linear algebra of programming ⋮ Probabilistic verification of Herman's self-stabilisation algorithm ⋮ Probabilistic may/must testing: retaining probabilities by restricted schedulers ⋮ Exploring probabilistic bisimulations. I ⋮ A unification of probabilistic choice within a design-based model of reversible computation ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Integrating stochastic reasoning into Event-B development ⋮ Mixed nondeterministic-probabilistic automata: blending graphical probabilistic models with nondeterminism ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Compositional noninterference from first principles ⋮ Automated reasoning for probabilistic sequential programs with theorem proving ⋮ Probabilistic Choice in Refinement Algebra ⋮ A probability perspective ⋮ Healthiness conditions for predicate transformers ⋮ Generating counterexamples for quantitative safety specifications in probabilistic B ⋮ Proofs of randomized algorithms in Coq ⋮ The shadow knows: refinement and security in sequential programs ⋮ On Higher-Order Probabilistic Subrecursion ⋮ Unnamed Item ⋮ Using probabilistic Kleene algebra pKA for protocol verification ⋮ How to Brew-up a Refinement Ordering ⋮ Data Refinement with Probability in Mind ⋮ Proof rules for the correctness of quantum programs ⋮ Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops ⋮ On the hardness of analyzing probabilistic programs ⋮ Algebraic reasoning for probabilistic action systems and while-loops ⋮ Toward automatic verification of quantum programs ⋮ Automated termination analysis of polynomial probabilistic programs ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Algorithmic probabilistic game semantics. Playing games with automata ⋮ Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language ⋮ Hidden-Markov program algebra with iteration ⋮ Refinement algebra for probabilistic programs ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Unnamed Item ⋮ Fifty years of Hoare's logic ⋮ Identity-Based Cryptosystems and Quadratic Residuosity ⋮ Probabilistic NetKAT ⋮ Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs ⋮ Measure Transformer Semantics for Bayesian Machine Learning ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular ⋮ Weakest preconditions in fibrations ⋮ Computing expected runtimes for constant probability programs ⋮ Predicate transformers for extended probability and non-determinism ⋮ A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language ⋮ Formalising Semantics for Expected Running Time of Probabilistic Programs ⋮ Reasoning about faulty quantum programs ⋮ Moment-based analysis of Bayesian network properties ⋮ Stepwise refinement of sequence diagrams with soft real-time constraints ⋮ Generating functions for probabilistic programs
