by least fixed points of certain continuous functions.
Whereas upper bounds are already well studied and simple
to infer in general, there is no widely-applicable rule for
determining lower bounds. In this talk, we will present the
first inductive rule for the inference of lower bounds on
expected outcomes of probabilistic programs by connecting
the results from fixed point theory with the Optional Stopping Theorem.