An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs

TL;DR

This paper presents a novel approach combining random testing and abstract interpretation to analyze probabilistic programs with nondeterminism, providing formulas for precision and discussing optimization.

Contribution

It introduces a new combined method for probabilistic program analysis, linking testing and abstract interpretation with theoretical formulas.

Findings

Effective analysis of probabilistic programs with nondeterminism

Formulas linking analysis precision to iterations

Experimental results demonstrating method's viability

Abstract

We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. After introducing "ordinary" testing, we show how to combine testing and abstract interpretation and give formulas linking the precision of the results to the number of iterations. We then discuss complexity and optimization issues and end with some experimental results.