Sat 21 Nov 2020 01:00 - 01:20 at SPLASH-I - F-4A Chair(s): Hidehiko Masuhara
We present a novel methodology for the automated resource analysis of non-deterministic,
probabilistic imperative programs, which gives rise to a \emph{modular approach}.
Program fragments are analysed in full independence.
Moreover, the established results allow us to incorporate sampling
from \emph{dynamic distributions}, making our analysis applicable to a wider class of examples, for
example the \emph{Coupon Collector's problem}.
We have implemented our contributions in the tool \ecoimp, 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. %MA: downscale superiority.
Our experiments show that our tool runs typically at least one \emph{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.