4 papers · 1 filter
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…
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…
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…
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…