Mora
Mora is an automated tool for generating invariants of probabilistic programs. Inputs to
Mora are so-called Prob-solvable loops that are 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.