Termination Analysis of Probabilistic Programs Through Positivstellensatz’s

DOI10.1007/978-3-319-41528-4_1zbMath1411.68025arXiv1604.07169OpenAlexW2435583538MaRDI QIDQ4633524

Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady

Publication date: 3 May 2019

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

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

Mathematics Subject Classification ID

Martingales with discrete parameter (60G42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Learning probabilistic termination proofs ⋮ A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ The probabilistic termination tool amber ⋮ Unnamed Item ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops ⋮ On the hardness of analyzing probabilistic programs ⋮ Automated termination analysis of polynomial probabilistic programs ⋮ Maximizing the Conditional Expected Reward for Reaching the Goal ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Nearly Optimal Verifiable Data Streaming