Backwards Abstract Interpretation of Probabilistic Programs

  • David Monniaux
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


In industrial contexts, safety regulations often mandate upper bounds on the probabilities of failure. Now that embedded computers are part of many indus- trial environments, it is often needed to analyze programs with non-deterministic and probabilistic behavior. We propose a general abstract interpretation based method for the static analysis of programs using random generators or random inputs. Our method also allows \ordinary" non-deterministic inputs, not neces- sarily following a random distribution.


Weight Function Abstract Interpretation Continuous Linear Operator Probabilistic Program Abstract Domain 
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.


  1. 1.
    François Bourdoncle. Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In PLILP’ 90, volume 456 of LNCS, pages 307–323. Springer-Verlag, 1990.Google Scholar
  2. 2.
    P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106–130. Dunod, Paris, France, 1976.Google Scholar
  3. 3.
    Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. J. Logic Prog., 2-3(13):103–179, 1992.CrossRefMathSciNetGoogle Scholar
  4. 4.
    Alessandra Di Pierro and Herbert Wiklicky. Concurrent constraint programming: Towards probabilistic abstract interpretation. In 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), 2000.Google Scholar
  5. 5.
    J.L. Doob. Measure Theory, volume 143 of Graduate Texts in Mathematics. Springer-Verlag, 1994.Google Scholar
  6. 6.
    Paul R. Halmos. Measure theory. The University series in higher mathematics. Van Nostrand, 1950.Google Scholar
  7. 7.
    Jifeng He, K. Seidel, and A. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2-3):171–192, April 1997. Formal specifications: foundations, methods, tools and applications (Konstancin, 1995).zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    D. Kozen. Semantics of probabilistic programs. In 20th Annual Symposium on Foundations of Computer Science, pages 101–114, Long Beach, Ca., USA, October 1979. IEEE Computer Society Press.Google Scholar
  9. 9.
    D. Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 22(3):328–350, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Serge Lang. Linear algebra. Springer-Verlag, New York, 1989.Google Scholar
  11. 11.
    Gavin Lowe. Representing nondeterminism and probabilistic behaviour in reactive processes. Technical Report TR-11-93, Oxford University, 1993.Google Scholar
  12. 12.
    David Monniaux. Abstract interpretation of probabilistic semantics. In Seventh International Static Analysis Symposium (SAS’00), number 1824 in Lecture Notes in Computer Science. Springer-Verlag, 2000. © Springer-Verlag.Google Scholar
  13. 13.
    David Monniaux. An abstract Monte-Carlo method for the analysis of probabilistic programs (extended abstract). In 28th Symposium on Principles of Programming Languages (POPL’ 01). Association for Computer Machinery, 2001. To appear.Google Scholar
  14. 14.
    Carroll Morgan, Annabelle McIver, Karen Seidel, and J. W. Sanders. Probabilistic predicate transformers. Technical Report TR-4-95, Oxford University, February 1995.Google Scholar
  15. 15.
    Carroll Morgan, Annabelle McIver, Karen Seidel, and J. W. Sanders. Refinement-oriented probability for CSP. Formal Aspects of Computing, 8(6):617–647, 1996.zbMATHCrossRefGoogle Scholar
  16. 16.
    Reuven Y. Rubinstein. Simulation and the Monte-Carlo Method. Wiley series in probabilities and statistics. John Wiley & Sons, 1981.Google Scholar
  17. 17.
    Walter Rudin. Real and Complex Analysis. McGraw-Hill, 1966.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • David Monniaux
    • 1
  1. 1.LIENSFrance

Personalised recommendations