Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
From MaRDI portal
Abstract: One of the main challenges in the analysis of probabilistic programs is to compute invariant properties that summarise loop behaviours. Automation of invariant generation is still at its infancy and most of the times targets only expected values of the program variables, which is insufficient to recover the full probabilistic program behaviour. We present a method to automatically generate moment-based invariants of a subclass of probabilistic programs, called Prob-Solvable loops, with polynomial assignments over random variables and parametrised distributions. We combine methods from symbolic summation and statistics to derive invariants as valid properties over higher-order moments, such as expected values or variances, of program variables. We successfully evaluated our work on several examples where full automation for computing higher-order moments and invariants over program variables was not yet possible.
Recommendations
- A complete invariant generation approach for P-solvable loops
- Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
- Solving invariant generation for unsolvable loops
- Invariant Generation for P-Solvable Loops with Assignments
- Moment-based invariants for probabilistic loops with non-polynomial assignments
- Automated generation of non-linear loop invariants utilizing hypergeometric sequences
- Synthesizing invariants by solving solvable loops
- Automatic Generation of Polynomial Loop Invariants
- Automatic generation of non-linear loop invariants
- An iterative method for generating loop invariants
Cites work
- A game-based abstraction-refinement framework for Markov decision processes
- Abstraction, Refinement and Proof for Probabilistic Systems
- Aligator.jl -- a Julia package for loop invariant generation
- Bounded model checking for probabilistic programs
- Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
- Finding polynomial loop invariants for probabilistic programs
- How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Linear-invariant generation for probabilistic programs: automated support for proof-based methods
- On the hardness of analyzing probabilistic programs
- Probabilistic CEGAR
- Probabilistic recurrence relations
- Reasoning Algebraically About P-Solvable Loops
- Synthesizing Probabilistic Invariants via Doob’s Decomposition
- Tail probabilities for randomized program runtimes via martingales for higher moments
- Termination analysis of probabilistic programs through Positivstellensatz's
- Termination of nondeterministic probabilistic programs
- The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
- Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities
Cited in
(20)- Analysis of Bayesian networks via prob-solvable loops
- Moment-based analysis of Bayesian network properties
- Generating functions for probabilistic programs
- Automated termination analysis of polynomial probabilistic programs
- Automatic Generation of Invariants for Circular Derivations in SUP(LA)
- Automatic generation of non-linear loop invariants
- Linear-invariant generation for probabilistic programs: automated support for proof-based methods
- Finding polynomial loop invariants for probabilistic programs
- 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
- Data-Driven Invariant Learning for Probabilistic Programs
- Probabilistic program verification via inductive synthesis of inductive invariants
- Exact and approximate moment derivation for probabilistic loops with non-polynomial assignments
- Data-driven invariant learning for probabilistic programs
- (Un)solvable loop analysis
- Deciding termination of simple randomized loops
- Verification of the CVM algorithm with a functional probabilistic invariant
This page was built for publication: Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3297595)
