Probabilistic Output Analysis by Program Manipulation

TL;DR

This paper introduces a static analysis method for deriving over-approximations of output probability distributions of programs with known input distributions, using program transformation techniques.

Contribution

It presents a novel program transformation approach to probabilistic output analysis that does not rely on Markov assumptions and produces closed-form over-approximations.

Findings

Produces a probability function as an intermediate expression

Transforms and approximates the function to obtain a closed-form expression

Applicable to programs with known input distributions without Markov property assumptions

Abstract

The aim of a probabilistic output analysis is to derive a probability distribution of possible output values for a program from a probability distribution of its input. We present a method for performing static output analysis, based on program transformation techniques. It generates a probability function as a possibly uncomputable expression in an intermediate language. This program is then analyzed, transformed, and approximated. The result is a closed form expression that computes an over approximation of the output probability distribution for the program. We focus on programs where the possible input follows a known probability distribution. Tests in programs are not assumed to satisfy the Markov property of having fixed branching probabilities independently of previous history.