47 citations · 48 across the 4 of their papers we have counts for
Showing 2019Show all
3 papers · 1 filter
cs.LO2019★ 1 cited
Termination of Triangular Polynomial Loops
Marcel Hark, Florian Frohn, Jürgen Giesl
We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring like , , or . The…
cs.LO2019
Computing Expected Runtimes for Constant Probability Programs
Jürgen Giesl, Peter Giesl, Marcel Hark
We introduce the class of constant probability (CP) programs and show that classical results from probability theory directly yield a simple decision procedure for (positive) almos…
cs.LO2019★ 47 cited
Aiming Low Is Harder -- Induction for Lower Bounds in Probabilistic Program Verification
Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl +1
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…