5 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…
A Calculus for Modular Loop Acceleration
Florian Frohn
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniq…
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…