Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
From MaRDI portal
Publication:3297595
DOI10.1007/978-3-030-31784-3_15zbMath1437.68041arXiv1905.02835OpenAlexW2982014993WikidataQ124212509 ScholiaQ124212509MaRDI QIDQ3297595
Ezio Bartocci, Laura Kovács, Miroslav Stankovič
Publication date: 20 July 2020
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1905.02835
Related Items
Moment-based invariants for probabilistic loops with non-polynomial assignments, Distribution estimation for probabilistic loops, The probabilistic termination tool amber, Solving invariant generation for unsolvable loops, Symbolic computation in automated program reasoning, Automated termination analysis of polynomial probabilistic programs, Moment-based analysis of Bayesian network properties, Generating functions for probabilistic programs
Uses Software
Cites Work
- Unnamed Item
- A game-based abstraction-refinement framework for Markov decision processes
- The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
- Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
- On the hardness of analyzing probabilistic programs
- Aligator.jl -- a Julia package for loop invariant generation
- Bounded model checking for probabilistic programs
- Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities
- Termination of nondeterministic probabilistic programs
- How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times
- Probabilistic CEGAR
- Probabilistic recurrence relations
- Termination Analysis of Probabilistic Programs Through Positivstellensatz’s
- Synthesizing Probabilistic Invariants via Doob’s Decomposition
- Abstraction, Refinement and Proof for Probabilistic Systems
- Linear-Invariant Generation for Probabilistic Programs:
- Finding Polynomial Loop Invariants for Probabilistic Programs
- Reasoning Algebraically About P-Solvable Loops
- Tail probabilities for randomized program runtimes via martingales for higher moments
