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.