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

Lecture notes in computer science, pp. 712–722

Abstract

Abstract We present the Loop Acceleration Tool (), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on the novel calculus from [10, 11] for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, uses a new approach based on unsat cores. We evaluate ’s power and performance by extensive experiments.

Authors 2

1. Florian Frohn corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

2. Jürgen Giesl corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany