4 citations · 7 across the 4 of their papers we have counts for
9 papers
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Florian Frohn, Jürgen Giesl
We present the new version of the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is b…
Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Fabian Meyer, Marcel Hark, Jürgen Giesl
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…
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 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…