Abstract
It is often useful to introduce probabilistic behavior in programs, either because of the use of internal random generators (probabilistic algorithms), either because of some external devices (networks, physical sensors) with known statistics of behavior. Previous works on probabilistic abstract interpretation have addressed safety properties, but somehow neglected probabilistic termination. In this paper, we propose a method to automatically prove the probabilistic termination of programs using exponential bounds on the tail of the distribution. We apply this method to an example and give some directions as to how to implement it. We also show that this method can also be applied to make unsound statistical methods on average running times sound.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P. Cousot and R. Cousot. Abstract intrepretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, CA, January 1977.
Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. J. Logic Prog., 2–3(13):103–179, 1992.
J.L. Doob. Measure Theory, volume 143 of Graduate Texts in Mathematics. Springer-Verlag, 1994.
Wassily Hoeffding. Probability inequalities for sums of bounded random variables. J. Amer. Statist. Assoc., 58(301):13–30, 1963.
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.
D. Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 22(3):328–350, 1981.
Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In ACM Symposium on Principles of Programming Languages, volume 28, pages 81–92. ACM press, January 2001.
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. Extended version on the author’s web site.
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), pages 93–101. Association for Computer Machinery, 2001.
Éric Goubault. Static analyses of floating-point operations. In Static Analysis (SAS’01), Lecture Notes in Computer Science, pages 234–259, Springer-Verlag, July 2001.
Walter Rudin. Real and Complex Analysis. McGraw-Hill, 1966.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monniaux, D. (2001). An Abstract Analysis of the Probabilistic Termination of Programs. In: Cousot, P. (eds) Static Analysis. SAS 2001. Lecture Notes in Computer Science, vol 2126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47764-0_7
Download citation
DOI: https://doi.org/10.1007/3-540-47764-0_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42314-0
Online ISBN: 978-3-540-47764-8
eBook Packages: Springer Book Archive