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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Camporesi, F., Feret, J., Koeppl, H., Petrov, T.: Automatic reduction of stochastic rules-based models in a nutshell. Amer. Inst. of Physics, AIP 1281(2) (2010)
Chadha, R., Viswanathan, M., Viswanathan, R.: Least Upper Bounds for Probability Measures and Their Applications to Abstractions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 264–278. Springer, Heidelberg (2008)
Coletta, A., Gori, R., Levi, F.: Approximating probabilistic behaviors of biological systems using abstract interpretation 229(1), 165–182 (2009)
Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. TCS 277(1-2), 47–103 (2002)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic and Comp. 2(4), 511–547 (1992)
Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? FMSD 35(3), 229–264 (2009)
D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and Refinement Strategies for Probabilistic Analysis. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 57–76. Springer, Heidelberg (2002)
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. FAC 6(5), 512–535 (1994)
Hehner, E.: Probabilistic Predicative Programming. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 169–185. Springer, Heidelberg (2004)
Hehner, E.: A probability perspective. FAC 23(4), 391–419 (2011)
Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390–406. Springer, Heidelberg (2010)
Klenke, A.: Probability Theory: A Comprehensive Course. Springer, Heidelberg (2007)
Kozen, D.: Semantics of probabilistic programs. JCSS 22, 328–350 (1981)
Kwiatkowska, M., Norman, G., Parker, D.: Using probabilistic model checking in systems biology. PER 35(4), 14–21 (2008)
McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Heidelberg (2005)
Meyn, S.: Control Techniques for Complex Networks. CUP (2007)
Monniaux, D.: Abstract Interpretation of Probabilistic Semantics. In: SAS 2000. LNCS, vol. 1824, pp. 322–340. Springer, Heidelberg (2000)
Monniaux, D.: Abstract interpretation of programs as Markov decision processes. SCP 58(1–2), 179–205 (2005)
Morgan, C., McIver, A., Seidel, K., Sanders, J.: Probabilistic predicate transformers. TOPLAS 18(3), 325–353 (1996)
Di Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic lambda-calculus and quantitative program analysis. JLC 15(2), 159–179 (2005)
Di Pierro, A., Wiklicky, H.: Concurrent constraint programming: towards probabilistic abstract interpretation. In: PPDP, pp. 127–138. ACM (2000)
Di Pierro, A., Wiklicky, H.: Probabilistic Abstract Interpretation and Statistical Testing (Extended Abstract). In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 211–212. Springer, Heidelberg (2002)
Roy, P., Parker, D., Norman, G., de Alfaro, L.: Symbolic magnifying lens abstraction in Markov decision processes. In: QEST 2008, pp. 103–112. IEEE (2008)
Smith, M.: Probabilistic abstract interpretation of imperative programs using truncated normal distributions 220(3), 43–59 (2008)
Wachter, B., Zhang, L.: Best Probabilistic Transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 362–379. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousot, P., Monerau, M. (2012). Probabilistic Abstract Interpretation. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)