1 citations · 4 across the 10 of their papers we have counts for
11 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 vecto…
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…
Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT
Nils Lommen, Éléanore Meyer, Jürgen Giesl
Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in…
Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (Short WST Version)
Nils Lommen, Eleanore Meyer, Jürgen Giesl
There exist several results on deciding termination and computing runtime bounds for triangular weakly non-linear loops (twn-loops). We show how to use results on such subclasses o…
Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
Nils Lommen, Jürgen Giesl
We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, f…
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Nils Lommen, Fabian Meyer, Jürgen Giesl
There exist several results on deciding termination and computing runtime bounds for triangular weakly non-linear loops (twn-loops). We show how to use results on such subclasses o…
Improving Automatic Complexity Analysis of Integer Programs
Jürgen Giesl, Nils Lommen, Marcel Hark +1
In earlier work, we developed an approach for automatic complexity analysis of integer programs, based on an alternating modular inference of upper runtime and size bounds for prog…