Loop Invariants and Algebraic Reasoning

Workshop On Loop Invariants and Algebraic Reasoning

Satellite Workshop at ICALP 2025

The Mathematics Canteen (Department of Mathematics, Aarhus Universitetsparken), at Ny Munkegade 116, 8000 Aarhus C

Aarhus, Denmark

Monday 07th July 2025

Workshop Registration Link

Aim

Reasoning about loops is a fundamental task in program analysis and verification. To this end, loop invariants are an indispensable tool. They help both to establish safety properties (e.g., proofs of non-reachability) and liveness properties (e.g., as supporting invariants in termination proofs). Beyer et al. [VMCAI 2007] go so far as to call the problem of automatic invariant generation ‘’the most important task in program verification. '’

There has been a resurgence of interest in computing the polynomial invariants for loops. In one direction, theoretical work has produced complete algorithms that will generate the invariant ideal for abstract classes of loops. In another direction, recent works have produced templates and heuristics aimed at generating some (but not necessarily all) the invariants of more general classes of loops with conditional branching, polynomial assignments, and probabilistic updates.

This workshop aims to span the divide between the aforementioned directions and bring together researchers from both communities.

Participation

To participate in-person, please register for the workshop through ICALP’s registration portal. To participate remotely over Zoom, please contact the organisers for further details.

Speakers, Talks, and Slides

(Click on a talk title for the abstract.)

  • Rida Ait El Manssour (Oxford)

    Algebraic invariants of rational linear loops

    Automatically generating loop invariants is essential for ensuring software correctness, yet it remains a challenging problem in general. In this talk, I will focus on a specific class of programs: branching-free loops with a single linear update. I will introduce a PSPACE algorithm that computes all algebraic relationships that consistently hold among program variables throughout the loop’s execution. Additionally, I will highlight how these results can be applied to verify proposed invariants, and discuss promising directions for extending this approach to loops with multiple linear updates.

    This is based on a project with George Kenison, Mahsa Shirmohammadi, and Anton Varonka.

  • Ruiwen Dong (Magdalen College, Oxford)

    S-unit equations in modules

    Let $M$ be a finitely presented module over a Laurent polynomial ring $R$. We consider S-unit equations over $M$: these are equations of the form $x_1 m_1 + \cdots + x_K m_K = m_0$, where the coefficients $m_i$ are in $M$ and the variables $x_i$ range over the set of monomials of $R$. When the Laurent polynomial ring $R$ has the base ring $\mathbb{Z}$, (that is, $R = \mathbb{Z}[X_1^{\pm}, \ldots, X_N^{\pm}]$), we show that it is undecidable whether a given S-unit equation over a given module $M$ admits a solution. When $R$ has the base ring $\mathbb{Z}/T\mathbb{Z}$ for some integer $T > 1$, (that is, $R = (\mathbb{Z}/T\mathbb{Z})[X_1^{\pm}, \ldots, X_N^{\pm}]$), we show that the problem of deciding whether a given S-unit equation over a given module $M$ admits a solution is Turing equivalent to solving a system of linear-exponential Diophantine equations over $\mathbb{Z}$.

    This talk is based on a paper in SODA'25 as well as ongoing work with Doron Shafrir.

  • Roland Guttenberg (TUM)

    Finite Rational Matrix Semigroups have at most Exponential Size

    Weighted Automata or equivalently semigroups of matrices are a model for while loops with linear updates. While it has been shown that the optimal polynomial invariants for matrix semigroups can be computed, the algorithms have prohibitively high complexity. In ongoing work together with Rida Ait El Manssour, Nathan Lhote, Mahsa Shirmohammadi and James Worrell we are attempting to tackle the complexity by giving algorithms for identifying and solving simple subcases.

    The first such simple but interesting subcase are finite semigroups. While it is known that if a group of n-by-n matrices is finite, then it has size at most 2^n n!, for semigroups the best known bound is double exponential. We reduce this bound to a single exponential and obtain a PSPACE algorithm for deciding finiteness of a given matrix semigroup. Our main tool, which is applicable for any matrix semigroup, is the PTIME computation of an irreducible component decomposition. This can be viewed as a kind of extension of the decomposition of a graph into strongly-connected components.

  • Toghrul Karimov (MPI-SWS)

    Applications of O-Minimality to Linear Loops

    The Termination Problem for linear while loops subsumes, among others, the famous Skolem Problem for linear recurrence sequences, and is consequently known to be decidable only in low dimensions (i.e. the number of program variables). We will discuss how o-minimality of real numbers equipped with arithmetic and exponentiation can be used to prove sweeping decidability results–that do not depend on the dimension–for certain robust variants of the classical decision problems of linear loops. This talk is largely based on the paper “Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers”, which will appear at ICALP25.

  • Nathan Lhote (Aix-Marseille University)

    Minimizing Cost Register Automata over a Field

    Weighted automata (WA) are an extension of finite automata that define functions from words to values in a given semiring. An alternative deterministic model, called Cost Register Automata (CRA), was introduced by Alur et al. It enriches deterministic finite automata with a finite number of registers, which store values, updated at each transition using the operations of the semiring. It is known that CRA with register updates defined by linear maps have the same expressiveness as WA. Previous works have studied the register minimization problem: given a function computable by a WA and an integer k, is it possible to realize it using a CRA with at most k registers? In this paper, we solve this problem for CRA over a field with linear register updates, using the notion of linear hull, an algebraic invariant of WA introduced recently by Bell and Smertnig. We then generalise the approach to solve a more challenging problem, that consists in minimizing simultaneously the number of states and that of registers. Last, while the linear hull was recently shown to be computable by Bell and Smertnig, no complexity bounds were given. To fill this gap, we provide two new algorithms to compute invariants of WA. This allows us to show that the register (resp. state-register) minimization problem can be solved in 2-ExpTime (resp. in NExpTime).

    This is joint work with Yahia Idriss Benalioua and Pierre-Alain Reynier

  • Fatemeh Mohammadi (KU Leuven)

    Algebraic tools for computing polynomial loop invariants

    Loop invariants are properties of a loop program that hold before and after each iteration of the loop. They are often employed to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, the generation of invariants becomes a crucial task for loops. I specifically focus on polynomial loops, where both the loop conditions and assignments within the loop are expressed as polynomials. Although computing polynomial invariants for general loops is undecidable, efficient algorithms have been developed for certain classes of loops. For instance, when all assignments within a while loop involve linear polynomials, the loop becomes solvable. In this talk, I will discuss the more general case where the polynomials exhibit arbitrary degrees. Applying tools from algebraic geometry, I present two algorithms designed to generate all polynomial invariants for a while loop, up to a specified degree. These algorithms differ based on whether the initial values of the loop variables are given or treated as parameters.

    This talk is based on joint work with Erdenebayar Bayarmagnai and Rémi Prébet.

  • Mahsa Naraghi (UniversitĂ© Paris CitĂ©)

    Algebraic Closure of Matrix Sets Recognized by 1-VASS

    We prove that for any one-dimensional vector addition system with states (1-VASS), equipped with an alphabet and a morphism into the monoid of d-by-d rational matrices, the Zariski closure of the image of its language under the morphism is computable. To achieve this, we adapt Imre Simon’s concept of factorisation trees—originally developed for finite monoids—to the infinite monoid of rational matrices by replacing idempotent elements with stable matrices. Using tools from multilinear algebra, we show that every sequence of matrices can be represented as the yield of a factorisation tree whose height is bounded by an explicit function of the matrix dimension.

    This work is in collaboration with Rida Ait El Manssour, Mahsa Shirmohammadi, and James Worrell.

  • Mohab Safey El Din (Sorbonne UniversitĂ©, CNRS, LIP6)

    Modern algorithms for one block quantifier elimination over the reals

    One block quantifier elimination algorithms take as input a formula which consists of a (universal or existential) quantifier on real variables arising in some input polynomial constraints. These algorithms compute a logically equivalent quantifier-free formula of polynomial constraints. This problem is known to be solvable since Tarski's original work on elementary algebra and geometry.

    Quantifier elimination arises frequently in problems related to algebraic reasoning From a geometric perspective, one-block quantifier elimination computes a description of the projection of the real solution set to polynomial constraints on some affine subspace.

    In this talk, I will describe a new one block quantifier algorithm which leverages this geometric perspective. This yields new complexity results and practical performances which outperform the current state-of-the-art algorithms on a large family of examples.

  • Sylvain Schmitz (UniversitĂ© Paris CitĂ©)

    Polynomial Ideals and Order Ideals

    There is a well-known connection between polynomial ideals and order ideals, which relates e.g. Hilbert's Basis Theorem and the ascending chain condition on polynomial ideals with Dickson's Lemma and the descending chain condition on order ideals.

    As an illustration of how this connection can be exploited to use complexity results on order ideals, I’ll revisit the results of Benedikt, Duff, Sharad, and Worrell [LICS 2017] on the complexity of the zeroness problem for general and invertible polynomial automata, using recent results obtained with SchĂĽtze [ICALP 2024]. As a second illustration, I will point to some open questions regarding the complexity of computing Gröbner bases.

  • Anton Varonka (TU Wien)

    Rational Loop Synthesis

    Polynomial (equality) invariants have proven to be helpful in the inductive arguments about loop programs. The class of such invariants enjoys good closure properties and most importantly, allows for a finite representation of the set of all polynomial invariants for a given loop program. Therefore, a question of special theoretical interest concerns the decidability/complexity of finding this representation.

    Notably, small changes in the program model can render the problem of generating all polynomial invariants undecidable. We discuss the landscape and focus on the question “What polynomials can be invariants of simple enough loops?”. In this talk, we consider the model of simple linear loops, where the update of the rational variable vector is given by a single rational matrix. Loops like these are exactly the linear dynamical systems, as known in the linear recurrence sequences community. We further restrict ourselves to the loops that attain infinitely many different vectors.

    In order to understand the polynomial invariants of simple linear loops, we turn to the problem of loop synthesis from desired polynomial equalities. That is, we ask whether there exists a simple linear loop that has a given polynomial invariant. In this setting, synthesising a loop also means finding a vector of initial values---no surprise that loop synthesis is as hard as Hilbert's Tenth Problem over the rationals.

    Our results concern the decidability of existence and, in addition, the algorithmic generation of loops from invariants. We will discuss special classes of input polynomials: quadratic equations and conjunctions of pure binomial equalities. Finally, we will introduce a bit-bounded version of loop synthesis--where the objective is to find a simple linear loop with input entries of a bounded size.

Schedule

(All times are CEST/UTC+02:00)

08:30–09:00 Registration

09:00–10:30 Talks

Coffee Break

11:00–12:30 Talks

Lunch

14:00–15:30 Talks

Coffee Break

16:00–17:30 Talks

Workshop Ends

Organisers

Loops Loop Invariants Invariant Generation Invariant Verification Algebraic Methods Workshop