Quantitative Program Analysis
Chris Hankin
Imperial College, London
We present a new approach to program analysis of probabilistic
transition systems. The approach uses classical notions from linear
algebra rather than the more usual order-theoretic notions. One
advantage of this new approach is that we can measure the difference
between different solutions. This has proved useful in the analysis
of security where many notions of non-interference are based on certain
kinds of process equivalence. In this introductory talk, we focus on
the lambda calculus.
We will start by reviewing the classical approach to program analysis based
on abstract interpretation. We will take (first-order) strictness analysis
as a running example. We extend the lambda calculus with a probabilistic
choice operator and then introduce a characterisation of
the reduction graph of a term as a linear operator on some suitably defined
vector space representing the set of terms. We introduce a new notion
of program analysis which we call probabilistic abstract interpretation.
We show how this framework may be used to study the strictness of
probabilistic terms.
