Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)

arXiv (Cornell University)

Abstract

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 based on a novel calculus for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, LoAT uses a new approach based on SMT solving and unsat cores. An extensive evaluation shows that LoAT is highly competitive with other state-of-the-art tools for proving non-termination. While no other tool is able to deduce worst-case lower bounds for full integer programs, we also demonstrate that LoAT significantly outperforms its predecessors.

Authors 2

1. Florian Frohn Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2 , RWTH Aachen University , Aachen , Germany

2. Jürgen Giesl Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2 , RWTH Aachen University , Aachen , Germany