Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes

TL;DR

This paper introduces a modular method to automatically estimate upper bounds on the expected runtime of probabilistic integer programs by analyzing program parts and variable sizes iteratively, implemented in the KoAT tool.

Contribution

It presents a novel modular approach for inferring expected runtime bounds of probabilistic integer programs, integrated into an open-source analysis tool.

Findings

Successfully computes upper bounds on expected runtimes.

Automates analysis of probabilistic integer programs.

Implemented in the KoAT tool for practical use.

Abstract

We present a novel modular approach to infer upper bounds on the expected runtime of probabilistic integer programs automatically. To this end, it computes bounds on the runtime of program parts and on the sizes of their variables in an alternating way. To evaluate its power, we implemented our approach in a new version of our open-source tool KoAT.