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 ap-propriate 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 par-ticular, 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 trun-cated 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 mea-sure, we generate a probabilistic trace whose states are labelled by measures, describing the distribution of the behaviour of loops to various degrees of precision