In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[.], translating a pre-expectation semantics into first-order constraints, susceptible to automation via standard methods. A crucial step is the use of logical variables, inspired by previous work on Hoare logics for recursive programs. Noteworthy, our methodology is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights. We have implemented this analysis in our prototype ev-imp. We provide ample experimental evidence of the prototype's algorithmic expressibility.

We present a novel methodology for the automated resource analysis of non-deterministic, probabilistic imperative programs, which gives rise to a modular approach . Program fragments are analysed in full independence. Moreover, the established results allow us to incorporate sampling from dynamic distributions , making our analysis applicable to a wider class of examples, for example the Coupon Collector’s problem . We have implemented our contributions in the tool , exploiting a constraint-solver over iterative refineable cost functions facilitated by off-the-shelf SMT solvers. We provide ample experimental evidence of the prototype’s algorithmic power. Our experiments show that our tool runs typically at least one order of magnitude faster than comparable tools. On more involved examples, it may even be 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 scalability of sorts. This effects into a wider class of examples, whose expected cost analysis can be thus be performed fully automatically.