  Probabilistic program analysis aims to quantify the probability that a given
program satisfies a required property. It has many potential applications, from
program understanding and debugging to computing program reliability, compiler
optimizations and quantitative information flow analysis for security. In these
situations, it is usually more relevant to quantify the probability of
satisfying/violating a given property than to just assess the possibility of
such events to occur.
  In this work, we introduce an approach for probabilistic analysis of open
programs (i.e. programs with undefined identifiers) based on game semantics and
model counting. We use a symbolic representation of algorithmic game semantics
to collect the symbolic constraints on the input data (context) that lead to
the occurrence of the target events (e.g. satisfaction/violation of a given
property). The constraints are then analyzed to quantify how likely is an input
to satisfy them. We use model counting techniques to count the number of
solutions (from a bounded integer domain) that satisfy given constraints. These
counts are then used to assign probabilities to program executions and to
assess the probability for the target event to occur at the desired level of
confidence. Finally, we present the results of applying our approach to several
interesting examples and illustrate the benefits they may offer.
