Synthesizing Probabilistic Invariants via Doob’s Decomposition

DOI10.1007/978-3-319-41528-4_3zbMath1411.68057arXiv1605.02765OpenAlexW3100287873MaRDI QIDQ4633526

Thomas Espitau, Justin Hsu, Luis María Ferrer Fioriti, Gilles Barthe

Publication date: 3 May 2019

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1605.02765

Mathematics Subject Classification ID

Martingales with discrete parameter (60G42) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Latticed \(k\)-induction with an application to probabilistic programs ⋮ Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops ⋮ Probabilistic Lipschitz analysis of neural networks ⋮ Maximizing the Conditional Expected Reward for Reaching the Goal ⋮ Nearly Optimal Verifiable Data Streaming ⋮ Moment-based analysis of Bayesian network properties ⋮ Quantitative static analysis of communication protocols using abstract Markov chains