MORA -- Automatic Generation of Moment-Based Invariants

TL;DR

MORA is an automated tool that generates moment-based invariants for probabilistic programs with polynomial assignments, combining symbolic computation and statistics to analyze properties like expectations and variances.

Contribution

It introduces MORA, the first tool to automatically generate higher-order moment invariants for probabilistic programs with polynomial assignments.

Findings

Successfully computes invariants for probabilistic loops.

Handles higher-order moments such as expectations and variances.

Integrates symbolic and statistical methods effectively.

Abstract

We introduce MORA, an automated tool for generating invariants of probabilistic programs. Inputs to MORA are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from symbolic computation and statistics, MORA computes invariant properties over higher-order moments of loop variables, expressing, for example, statistical properties, such as expected values and variances, over the value distribution of loop variables.