Marcel Hark: Automated Runtime Analysis of Probabilistic Programs
In his dissertation, Marcel Hark developed a novel modular approach to infer upper bounds on the expected runtimes of probabilistic integer programs automatically. It computes bounds on the runtimes of program parts and on the sizes of their variables in an alternating way. To demonstrate its power and practical applicability, the approach was implemented in the tool KoAT. In contrast to upper bounds, the computation of lower bounds for probabilistic programs had been largely unexplored. Jointly with Kaminski, Hark developed the first inductive proof rule to verify such lower bounds on (possibly unbounded) expected values of random variables for probabilistic programs. An important question is whether there are classes of (sub-)programs where termination and complexity questions are decidable. Up to now, most of these results were restricted to non-probabilistic loops with linear arithmetic. Hark identified a new class of possibly non-linear programs and proved decidability results for both the halting and the (universal) termination problem, and he obtained the first computability results on the runtime complexity of such programs. In addition, he developed some of the first such decidability results for probabilistic programs. He discovered a class of probabilistic programs where (positive) almost-sure termination is decidable and where he could give a general formula for the exact expected runtime of any program in this class.