  In this article, we present a semantics-level adaption of the Optional
Stopping Theorem, sketch an expected-cost analysis as its application, and
survey different variants of the Optional Stopping Theorem that have been used
in static analysis of probabilistic programs.
