MORA -- Automatic Generation of Moment-Based Invariants
Formal Languages and Automata Theory
2021-03-09 v1 Programming Languages
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.
Cite
@article{arxiv.2103.03908,
title = {MORA -- Automatic Generation of Moment-Based Invariants},
author = {Ezio Bartocci and Laura Kovacs and Miroslav Stankovic},
journal= {arXiv preprint arXiv:2103.03908},
year = {2021}
}