Probabilistic program analysis – Matthew Dwyer

What is a probabilistic program? The classic view was introduced by Kozen. Imagine your favorite existing programming language enriched with a primitive that draws from a probability distribution, e.g. normal(0,1). Many programs are probabilistic in some way, as their inputs are distributed in a certain way. More modern probabilistic systems use an observe statement, which is very similar to an assert statement, but Mat is mostly talking about the classic view today.

A fun way to think about a program is a thing to change one probability distribution into another. For example if you have a odd/even function for natural numbers, the program changes a normal distribution over {-inf,inf} to a flat one over {0,1}.

This briefing is about probabilistic (program analysis) not (probabilistic program) analysis 🙂 So, we are going to probabilistically analyzing programs, not analyzing probabilistic programs. So what type of things can we analyze with probabilities?

Key concepts in data flow analysis and symbolic execution
(disclaimer: for the purpose of the briefing some corners are cut)

Programs are generators of a traces, that you can think about as either a list of states s, or a list of transitions.

An example:

Even this simple example has a gigantic number of possible traces, but we can quickly abstract into the two cases: true or false, that allows us to collapse 2^32-1 cases to just 2. Frameworks for these types of abstractions have been studied for nearly 50 years. Check out Kildall’s wikipedia page, says Mat, who introduced a data flow framework in 1973.

Abstractions

An ‘abstraction’ is a mapping from the input values of a program to a smaller abstract domain. An example is the forgetful abstraction that maps all input values to the same value. This seems useless, but is actually used quite often. But, an abstract domain is not enough, we need to lift operations from the lower, program level to the abstract domain.

Want to dive into this? Have a look at this paper, that describes an algorithm to compute the best abstract transformer for you.

Let’s look at our example program again.

Different domains can give rise to different analysis results. A good choice of domain is subtle and will take into account the semantics of the program. Want to know more? Read David Schmidt’s POPL 1999 paper.

Symbolic execution

In symbolic execution we are storing a map from program locations to symbolic expressions over program input variables, plus a path condition that is the conjunction of all encountered branch conditions so far. A SMT solver is used to determine whether the conjunction can be true. This is a nice application of an SAT solver I can use for my next talk 🙂 The difference with the above is that there is no guarantee that all states are reached, it is an underapproximation. Path explosion limits the ability to cover all paths, so most of the implementations use some sort of heuristic to choose what path to inspect.

Probabilities

So how do probabilities fit in this story? Probabilities are used to quantify the chance that each of the values in set occurs.

The idea, like described before is to think about a program as a transformer of one distribution into the other. Want to start? Check out the PRISM a probabilistic model checker.