47 citations · 65 across the 16 of their papers we have counts for
6 papers · 1 filter
Inferring Lower Runtime Bounds for Integer Programs
Florian Frohn, Matthias Naaf, Marc Brockschmidt +1
We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-rec…
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…
Termination of Triangular Integer Loops is Decidable
Florian Frohn, Jürgen Giesl
We consider the problem whether termination of affine integer loops is decidable. Since Tiwari conjectured decidability in 2004, only special cases have been solved. We complement…
Proving Non-Termination via Loop Acceleration
Florian Frohn, Jürgen Giesl
We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to a…
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…
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…