19/01/2020

Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification

Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen

Keywords: probabilistic programs, uniform integrability, weakest preexpectation, lower bounds, optional stopping theorem, verification, weakest precondition

Abstract: We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule is simple in the sense that loop body semantics need to be applied only finitely often in order to verify that the candidates are indeed lower bounds. In particular, it is not necessary to find the limit of a sequence as in many previous rules.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at POPL 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers