We present a novel methodology for the automated resource analysis of non-deterministic, probabilistic imperative programs, based on three ingredients: (i) a refinement of the ert-calculus of Kaminski et al. to reason about expected costs; (ii) an integration of an expected value analysis within this calculus; and (iii) a constraint-solver over iterative refineable cost functions facilitated by off-the-shelf SMT-solvers.

This gives a unique modular approach to the problem at hand. Program fragments can be analysed in full independence. Further, it allows us to incorporate sampling from dynamic distributions, making our analysis more realistic.

All of this has been implemented in the tool eco-imp. Our experiments show that our tool runs on average orders of magnitude faster than comparable tools: execution times of several seconds become milliseconds. It is also the first tool that can provide a fully automated analysis of the Coupon Collector’s problem, whose formalisation requires sampling from dynamic distributions.