Title
Compositionality and Relationality in Quantitative Program Analysis


Abstract

Herbert Wiklicky, Imperial College London joint work with

Alessandra Di Pierro, Universita' di Verona

Chris Hankin, Imperial College London

We discuss basic ideas for defining a collecting semantics for a simple (imperative) probabilistic language - pWhile. The aim is to construct in a syntax-directed way the generator of a (discrete time) Markov chain which corresponds to the stochastic process which realises the behaviour of any given pWhile program. In this so-called Linear Operator Semantics (LOS) the notion of a tensor product plays a central role which allows for a straight forward definition of the semantics of a program. Although this might be theoretically quite satisfying, the (potential) exponential increase in size makes this representation of the semantics infeasible for practical applications like static program analysis. To remedy this, we will show how to apply Probabilistic Abstract Interpretation (PAI) in order to ``simplify'' the LOS substantially. In this context we are able, for example, to extract abstract branching probabilities (which could be utilised e.g. for speculative threading) and to quantify or measure the relational dependency between different program properties (as statistical correlation).