The paper entitled “Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms” by Benjamin Kaminski, Joost-Pieter Katoen, Christoph Matheja and Federico Olmedo has been accepted for the prestigious journal Journal of the ACM. This paper presents a wp–style calculus for obtaining bounds on the expected run time of randomized algorithms.Its application includes determining the (possibly infinite) expected termination time of a randomized algorithm and proving positive almost–sure termination—does a program terminate with probability one in finite expected time?

The paper is an extended version of the ESOP 2016 conference paper that was awarded with the EATCS Best Paper Award at ETAPS 2016.