3 citations · 13 across the 20 of their papers we have counts for
21 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…
Deciding Termination of Simple Randomized Loops
Éléanore Meyer, Jürgen Giesl
We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a…
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl +1
We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a se…
The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Jürgen Giesl
Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems automatically. We adapt dependency pairs to the probabilistic setting and de…
Small Term Reachability and Related Problems for Terminating Term Rewriting Systems
Franz Baader, Jürgen Giesl
Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small t…
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…
Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Jürgen Giesl
Dependency pairs (DPs) are one of the most powerful techniques for automated termination analysis of term rewrite systems. Recently, we adapted the DP framework to the probabilisti…
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…
From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Florian Frohn, Jürgen Giesl
There are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist wh…
A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Stefan Dollase, Jürgen Giesl
Recently, the well-known dependency pair (DP) framework was adapted to a dependency tuple framework in order to prove almost-sure innermost termination (iAST) of probabilistic term…
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…
Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)
Jan-Christoph Kassing, Jürgen Giesl
Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabil…
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…
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
Jan-Christoph Kassing, Jürgen Giesl
Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabil…
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…