Abstract
We present 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 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, LoAT uses a new approach based on unsat cores. We evaluate LoAT’s power and performance by extensive experiments.
Cite
CITATION STYLE
Frohn, F., & Giesl, J. (2022). Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13385 LNAI, pp. 712–722). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-10769-6_41
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
