A modular cost analysis for probabilistic programs

We present a novel methodology for the automated resource analysis of non-deterministic, probabilistic imperative programs, which gives rise to a unique modular approach. Program fragments are analysed in full independence. Further, the results established allow us to incorporate sampling from dynamic distributions, making our analysis applicable to realistic examples.

We have implemented our contributions in the tool eco-imp, exploiting a constraint-solver over iterative refineable cost functions facilitated by off-the-shelf SMT-solvers. We provide ample experimental evidence of the prototypes' algorithmic superiority. Our experiments show that our tool runs typically at least one order of magnitude faster than comparable tools. On realistic examples, it is even the case that execution times of seconds become milliseconds. At the same time we retain the precision of existing tools.

The extensions in applicability and the greater efficiency of our prototype, yield scalabilty of the tool. This effects into more realistic examples, whose expected cost analysis can be thus performed fully automatically. In particular, our tool is the first establishing an automated analysis of the Coupon Collector's problem.