Abstract:
Abstract interpretation has been widely used for verifying properties of computer systems. Here, we present a way to extend this framework to the case of probabilistic systems.
The probabilistic abstraction framework that we propose allows us to systematically lift any classical analysis or verification method to the probabilistic setting by separating in the program semantics the probabilistic behavior from the (non-)deterministic behavior. This separation provides new insights for designing novel probabilistic static analyses and verification
methods.
We define the concrete probabilistic semantics and propose different ways to abstract them. We provide examples illustrating the expressiveness and effectiveness of our approach.
\bibitem{CousotMonerau-ESOP2012-PAI}
Patrick Cousot and Micha\"el Monerau.
\newblock Probabilistic Abstract Interpretation.
\newblock In H.~Seidel, editor, \emph{22nd European Symposium on
Programming (ESOP 2012)}, Lecture Notes in Computer Science,
vol. 7211, pages 166--190, Springer-Verlag, Heidelberg, 2012.
@inproceedings{CousotMonerau-ESOP2012-PAI,
author = "Patrick Cousot and Micha\"el Monerau",
title = "Probabilistic Abstract Interpretation",
booktitle = "22nd European Symposium on Programming (ESOP 2012)",
editor = "H.~Seidel",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
volume = "7211",
year = 2012,
pages = "166--190",
address = "Heidelberg"
}