Probabilistic Abstract Interpretation of Imperative Programs using Truncated Normal Distributions

When modelling a complex system, such as one with distributed functionality, we need to choose an appropriate level of abstraction. When analysing quantitative properties of the system, this abstraction is typically probabilistic, since we introduce uncertainty about its state and therefore its behaviour. In particular, when we aggregate several concrete states into a single abstract state we would like to know the distribution over these states. In reality, any probability distribution may be possible, but this leads to an intractable analysis. Therefore, we must find a way to approximate these distributions in a safe manner.We present an abstract interpretation for a simple imperative language with message passing, where truncated multivariate normal distributions are used as the abstraction. This allows the probabilities of transient properties to be bounded, without needing to calculate the exact distribution. We describe the semantics of programs in terms of automata, whose transitions are linear operators on measures. Given an input measure, we generate a probabilistic trace whose states are labelled by measures, describing the distribution of the values of variables at that point. By the use of appropriate widening operators, we are able to abstract the behaviour of loops to various degrees of precision