Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops

Ezio Bartocci, Laura Kovács, Miroslav Stankovič

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…