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 explain how to implement it.
We also show that
this method can also be applied to make unsound statistical methods on
average running times sound.
