1 citations · 4 across the 13 of their papers we have counts for
19 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…
Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks
Jan-Christoph Kassing, Henri Nagel, Alexander Schlecht +1
In recent years, numerous techniques were developed to automatically prove termination of different kinds of probabilistic programs. However, there are only few automated methods t…
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…
Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Leon Spitzer, Jürgen Giesl
The dependency pair (DP) framework is one of the most powerful techniques for automatic termination and complexity analysis of term rewrite systems. While DPs were extended to prov…