Lecture Notes in Computer Science, 2001, Volume 2126/2001, 111-126, DOI: 10.1007/3-540-47764-0_7

An Abstract Analysis of the Probabilistic Termination of Programs

David Monniaux

View Related Documents

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.

Fulltext Preview

Image of the first page of the fulltext document