activity
20242026
most citedAccelerating Loops with Arrays

1 citations · 1 across the 3 of their papers we have counts for

collaborators

7 papers

cs.LO2026

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…

cs.LO20261 cited

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…

cs.LO2026

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…

cs.LO2026

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

cs.LO2025

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…

cs.LO2025

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