| | | | |
|

Abstract interpretation of probabilistic semantics
by David Monniaux.
Abstract
Following earlier models, we lift standard deterministic and
nondeterministic semantics of imperative programs to probabilistic semantics.
This semantics allows for random external inputs of known or
unknown probability and random number generators.
We then propose a method of analysis of programs according to this
semantics, in the general framework of abstract interpretation. This
method lifts an "ordinary" abstract lattice, for non-probabilistic programs,
to one suitable for probabilistic programs.
Our construction is highly generic. We discuss the in
uence of certain
parameters on the precision of the analysis, basing ourselves on experimental
results.
Files
|
|
|