Measuring the Precision of Abstract Interpretations

We present a method for approximating the semantics of probabilistic programs to the purpose of constructing semantics-based analyses of various properties. The method is also suited for a probabilistic analysis of classical deterministic programs. The framework resembles the one based on Galois connection used in abstract interpretation, the main difference being the choice of linear space structures instead of order-theoretic ones as semantical (concrete and abstract) domains. Linear spaces reflect the quantitative aspects of (probabilistic) computation and are therefore of fundamental importance in the semantics and the semantics-based analysis. The intrinsic quantitative nature of linear spaces makes the method suitable for investigations on the problem of a numerical comparison of abstract interpretations with respect to their precision.