10 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…
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…
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…