3 citations · 10 across the 11 of their papers we have counts for
18 papers
Proceedings of the 21st International Workshop on Termination
Florian Frohn, Étienne Payet
This report contains the proceedings of the 21st International Workshop on Termination (WST 2026), which was held in Lisbon on July 25. It was affiliated with the 13th Internationa…
Accelerating Loops with Arrays
Florian Frohn, Jürgen Giesl
We propose a novel acceleration technique for loops operating on arrays. The goal of acceleration is to characterize the transitive closure of loops in a logic which is suitable fo…
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…
Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
Emanuele De Angelis, Florian Frohn
This volume contains the post-proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2025), which took place in Zagreb, Croatia, on July 22, 2025, as…
Infinite State Model Checking by Learning Transitive Relations
Florian Frohn, Jürgen Giesl
We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until cons…
Satisfiability Modulo Exponential Integer Arithmetic
Florian Frohn, Jürgen Giesl
SMT solvers use sophisticated techniques for polynomial (linear or non-linear) integer arithmetic. In contrast, non-polynomial integer arithmetic has mostly been neglected so far.…
Integrating Loop Acceleration into Bounded Model Checking
Florian Frohn, Jürgen Giesl
Bounded Model Checking (BMC) is a powerful technique for proving unsafety. However, finding deep counterexamples that require a large bound is challenging for BMC. On the other han…
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…
Proving Non-Termination by Acceleration Driven Clause Learning (Short WST Version)
Florian Frohn, Jürgen Giesl
We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to disprove term…
Proving Non-Termination by Acceleration Driven Clause Learning
Florian Frohn, Jürgen Giesl
We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to transition sy…
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
Florian Frohn, Jürgen Giesl
Constrained Horn Clauses (CHCs) are often used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On…
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Florian Frohn, Jürgen Giesl
We present the new version of the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is b…
A Calculus for Modular Loop Acceleration and Non-Termination Proofs
Florian Frohn, Carsten Fuhs
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed.…
A Calculus for Modular Loop Acceleration
Florian Frohn
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniq…
Inferring Lower Runtime Bounds for Integer Programs
Florian Frohn, Matthias Naaf, Marc Brockschmidt +1
We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-rec…
Termination of Triangular Polynomial Loops
Marcel Hark, Florian Frohn, Jürgen Giesl
We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring like , , or . The…
Termination of Triangular Integer Loops is Decidable
Florian Frohn, Jürgen Giesl
We consider the problem whether termination of affine integer loops is decidable. Since Tiwari conjectured decidability in 2004, only special cases have been solved. We complement…
Proving Non-Termination via Loop Acceleration
Florian Frohn, Jürgen Giesl
We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to a…