Abstract Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Rodríguez-Carbonell and Kapur (in: Proceedings of the ISSAC, pp 266–273, 2004), one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

Displayed equation in Definition 71.1 Online version 1.2 Revision L(x, y) = L if x depends linearly on y, and N if x depends nonlinearly on y.L(x, y) ∶= L if x depends linearly on y, and N if x depends non-linearly on y.

We present a novel static analysis technique to derive higher moments for program variables for a large class of probabilistic loops with potentially uncountable state spaces. Our approach is fully automatic, meaning it does not rely on externally provided invariants or templates. We employ algebraic techniques based on linear recurrences and introduce program transformations to simplify probabilistic programs while preserving their statistical properties. We develop power reduction techniques to further simplify the polynomial arithmetic of probabilistic programs and define the theory of moment-computable probabilistic loops for which higher moments can precisely be computed. Our work has applications towards recovering probability distributions of random variables and computing tail probabilities. The empirical evaluation of our results demonstrates the applicability of our work on many challenging examples.

We use algebraic reasoning to translate Bayesian network (BN) properties into linear recurrence equations over statistical moments of BN variables. We show that this translation can always be done for various BNs, such as discrete, Gaussian, conditional linear Gaussian, and dynamic BNs. An important part of our work comes with representing BNs as while loops in probabilistic programs with polynomial assignments over random variables and parametrised distributions. We prove that closed-form summaries of probabilistic loops precisely characterize higher-order moments of BN variables. As such, we automatically solve several BN-related problems, including exact inference, sensitivity analysis, filtering, and computing the expected number of rejecting samples in sampling-based procedures. We evaluate our work on a number of BN benchmarks, using automated invariant generation within Prob-solvable loop analysis. This paper is an extended version of the “Analysis of Bayesian Networks via Prob-Solvable Loops” manuscript published at ICTAC 2020 [1].

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.