9 papers
KoAT: Automatic Complexity and Termination Analysis of Integer Programs
Nils Lommen, Ãléanore Meyer, Jürgen Giesl
KoAT is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, KoAT implements an alternating modular inferenc…
Verifying LTL for Infinite State Systems via Termination Analysis
Nils Lommen, Moritz Leven Rosarius, Jürgen Giesl
We show that existing tools for termination analysis are extremely well suited for LTL model checking of infinite state systems. To this end, we present a framework MoAT which uses…
Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems
Christopher Brix, Julia Walczak, Nils Lommen +1
Solving quantifier-free non-linear real arithmetic (NRA) problems is a computationally hard task. To tackle this problem, prior work proposed a promising approach based on gradient…
On Deciding Constant Runtime of Linear Loops
Florian Frohn, Jürgen Giesl, Peter Giesl +1
We consider linear single-path loops of the form \[ \textbf{while} \quad Ï\quad \textbf{do} \quad \vec{x} \gets A \vec{x} + \vec{b} \quad \textbf{end} \] where is a vect…
Modular Automatic Complexity Analysis of Recursive Integer Programs
Nils Lommen, Jürgen Giesl
In earlier work, we developed a modular approach for automatic complexity analysis of integer programs. However, these integer programs do not allow non-tail recursive calls or sub…
Targeting Completeness: Automated Complexity Analysis of Integer Programs
Nils Lommen, Ãléanore Meyer, Jürgen Giesl
There exist several approaches to infer runtime or resource bounds for integer programs automatically. In this paper, we study the subclass of periodic rational solvable loops (prs…