# From Affine to Polynomial: Synthesizing Loops with Branches via Algebraic Geometry

Erdenebayar Bayarmagnai, Fatemeh Mohammadi, Rémi Prébet

► To cite this version:

Erdenebayar Bayarmagnai, Fatemeh Mohammadi, Rémi Prébet. From Affine to Polynomial: Synthesizing Loops with Branches via Algebraic Geometry. 2025. hal-05296092

HAL Id: hal-05296092

https://hal.science/hal-05296092v1

Preprint submitted on 3 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# From Affine to Polynomial: Synthesizing Loops with Branches via Algebraic Geometry

Erdenebayar Bayarmagnai · Fatemeh Mohammadi · Rémi Prébet

**Abstract** Ensuring software correctness remains a fundamental challenge in formal program verification. One promising approach relies on finding polynomial invariants for loops. Polynomial invariants are properties of a program loop that hold before and after each iteration. Generating such invariants is a crucial task in loop analysis, but it is undecidable in the general case. Recently, an alternative approach to this problem has emerged, focusing on synthesizing loops from invariants. However, existing methods only synthesize affine loops without guard conditions from polynomial invariants. In this paper, we address a more general problem, allowing loops to have polynomial update maps with a given structure, inequations in the guard condition, and polynomial invariants of arbitrary form.

We use algebraic geometry tools to design and implement an algorithm that computes a finite set of polynomial equations whose solutions correspond to all non-deterministic branching loops satisfying the given invariants. Furthermore, we introduce a new class of invariants for which we present a significantly more efficient algorithm. In other words, we reduce the problem of synthesizing loops to find solutions of multivariate polynomial systems with rational entries. This final step is handled in our software using an SMT solver.

## 1 Introduction

Loop invariants are properties that hold before and after each iteration of a loop. They play a central role in automating program verification, which guarantees program correctness prior to execution. Various well-established methods rely on loop invariants for safety verification, including the Floyd-Hoare inductive assertion technique [1] and termination verification using standard ranking functions [2]. When a loop invariant takes the form of a polynomial equation or inequality, it is referred to as a polynomial invariant. In this paper, we restrict our attention to invariants given by polynomial equations.

In this work, instead of generating polynomial invariants for a given loop, we address the reverse problem, that is synthesizing a loop that satisfies a specified set of polynomial invariants.

We consider polynomial loops $\mathcal{L}(\mathbf{a}, h, F)$ of the form

$$ \mathbf{x} := (x_1, \dots, x_n) \leftarrow \mathbf{a} := (a_1, \dots, a_n) \\ \mathbf{while} \ h(\mathbf{x}) \neq 0 \ \mathbf{do} \\ \qquad \begin{pmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end{pmatrix} \leftarrow^F \begin{pmatrix} F_1 \\ F_2 \\ \vdots \\ F_n \end{pmatrix} \\ \mathbf{end while} $$

Here, $x_i$ are the program variables with initial values $a_i$, $h \in \mathbb{C}[\mathbf{x}]$, and $F = (F_1, \dots, F_n)$ is a sequence of polynomials in $\mathbb{C}[\mathbf{x}]$. The condition $h(\mathbf{x}) \neq 0$, called the *guard*, is assumed to be a single inequation for simplicity. This is without loss of generality, since a guard of the form $h_1 \neq 0, \dots, h_k \neq 0$ can be replaced by the product condition $h_1 \cdots h_k \neq 0$. When no guard is present, we write $\mathcal{L}(\mathbf{a}, 1, F)$, which corresponds to an infinite loop.

In the following, we introduce some terminology from algebraic geometry. For further details, we refer the
reader to [3,4,5]. We denote the field of complex numbers by $\mathbb{C}$. Throughout the paper, $\mathbf{x}$ denotes the tuple of indeterminates $x_1, \dots, x_n$, and $\mathbb{C}[\mathbf{x}]$ the multivariate polynomial ring in these variables.

**Ideals.** A polynomial ideal $I$ is a subset of $\mathbb{C}[\mathbf{x}]$ that is closed under addition, $0 \in I$ and for any $f \in \mathbb{C}[\mathbf{x}]$ and $g \in I$, $fg \in I$. Given a subset $S$ of $\mathbb{C}[\mathbf{x}]$, the ideal generated by $S$ is

$$ \langle S \rangle = \{a_1 f_1 + \dots + a_m f_m \mid a_i \in \mathbb{C}[\mathbf{x}], f_i \in S, m \in \mathbb{N}\}. $$

By Hilbert Basis Theorem [3, Theorem 4, Chap. 2], every ideal is generated by finitely many polynomials. For a subset $X \subset \mathbb{C}^n$, the defining ideal $I(X)$ of $X$ is the set of polynomials that vanish on $X$. The radical ideal of an ideal $I \subset \mathbb{C}[\mathbf{x}]$ is defined as

$$ \sqrt{I} = \{f \in \mathbb{C}[\mathbf{x}] \mid f^m \in I \text{ for some } m \in \mathbb{N}\}. $$

**Varieties.** For $S \subset \mathbb{C}[\mathbf{x}]$, the algebraic variety $V(S)$ is the common zero set of all polynomials in $S$. Moreover, $V(S) = V(\langle S \rangle)$ and so every algebraic variety is the vanishing locus of finitely many polynomials.

**Polynomial maps.** A map $F : \mathbb{C}^n \to \mathbb{C}^m$ is a polynomial map if there exist $f_1, \dots, f_m \in \mathbb{C}[x_1, \dots, x_m]$ such that

$$ F(x) = (f_1(x), \dots, f_m(x)) $$

for all $x \in \mathbb{C}^n$. For simplicity, we will identify polynomial maps and their corresponding polynomials.

In the following definition, $F^{(l)}(x)$ is defined recursively as $F^{(l)}(x) = F(F^{(l-1)}(x))$ for any $l > 1$ and $F^{(0)}(x) = x$ by convention.

**Definition 1** A polynomial $g$ is an invariant of the loop $\mathcal{L}(\mathbf{a}, h, F)$ if, for any $m \in \mathbb{Z}_{\ge 0}$, either

$$ g(F^{(m)}(\mathbf{a})) = 0, $$

or there exists $m \in \mathbb{Z}_{\ge 0}$ such that

$$ g(F^{(m)}(\mathbf{a})) = h(F^{(m)}(\mathbf{a})) = 0, $$

and for every $0 \le l < m$

$$ g(F^{(l)}(\mathbf{a})) = 0 \text{ and } h(F^{(l)}(\mathbf{a})) \neq 0. $$

**Definition 2** Let $\mathcal{L}(\mathbf{a}, h, F)$ be a polynomial loop. The set of all polynomial invariants for $\mathcal{L}(\mathbf{a}, h, F)$ is called the invariant ideal of $\mathcal{L}$ and is denoted by $I_{\mathcal{L}(\mathbf{a}, h, F)}$.

The invariant ideal is indeed known (e.g. [6]) to be an ideal of $\mathbb{C}[x_1, \dots, x_n]$ where $x_1, \dots, x_n$ are the program variables. Consider polynomials $f_1, \dots, f_n$ in $\mathbb{C}[x_1, \dots, x_n]$, then we will denote by

$$ \operatorname{span}\{f_1, \dots, f_n\} $$

the vector space they generate.

**Definition 3** Let $\mathbf{f}_1 = (f_{1,1}, \dots, f_{1,l_1}), \dots, \mathbf{f}_n = (f_{n,1}, \dots, f_{n,l_n})$ and $(F_1, \dots, F_n)$ be sequences of polynomials in $\mathbb{C}[\mathbf{x}]$ such that for every $i$,

$$ F_i = \sum_{j=1}^{l_i} b_{i,j} f_{i,j} $$

for some $b_{i,j} \in \mathbb{C}$. Let $\mathbf{f} = (\mathbf{f}_1, \dots, \mathbf{f}_n)$ and define a map

$$ F_{\mathbf{f},\mathbf{b}} : \mathbb{C}^n \to \mathbb{C}^n $$

with $F_{\mathbf{f},\mathbf{b}}(x) = (F_1(x), \dots, F_n(x))$.

The object defined below is the primary focus of this paper. We prove that it is an algebraic variety and compute the polynomial equations that define it.

**Definition 4** Using the notation of Definition 3, let $h \in \mathbb{C}[\mathbf{x}]$, $g = (g_1, \dots, g_m)$ be a sequence of polynomials in $\mathbb{C}[\mathbf{x}]$, and $\mathbf{a} \in \mathbb{C}^n$. The coefficient set of the polynomial loop structured by $\mathbf{f}$ with invariants $g$ is defined as

$$ \mathcal{C}(\mathbf{a}, h, \mathbf{f}; g) = \{ \mathbf{b} \in \mathbb{C}^{l_1+\dots+l_n} \mid g \subset I_{\mathcal{L}(\mathbf{a},h,F_{\mathbf{f},\mathbf{b}})} \}. $$

In simple words, $\mathcal{C}(\mathbf{a}, h, \mathbf{f}; g)$ is the set of all coefficient vectors $\mathbf{b} \in \mathbb{C}^{l_1+\dots+l_n}$ such that all polynomials in $g$ are polynomial invariants of the following loop:

```
x $\leftarrow$ a
while $h(\mathbf{x}) \neq 0$ do
x $\leftarrow$ $F_{\mathbf{f},\mathbf{b}}(\mathbf{x})$
end while
```

In prior works [7,8,9], restricting computations to affine loops corresponds to choose $\mathbf{f}_i = (1, x_1, \dots, x_n)$, for all $1 \le i \le n$.

**Related work.** The computation of polynomial invariants for loops has been an active area of research over the past two decades [10, 11, 12, 13, 14, 6, 15, 16, 17]. However, computing invariant ideals is undecidable for general loops [18]. Consequently, efficient methods have been developed for restricted classes of loops, particularly those in which the assertions are linear or can be reduced to linear form.

The converse problem, namely synthesizing loops from given invariants, has received considerably less attention in the literature. Most existing work has focused on linear and affine loops. Synthesizing linear loops that satisfy given invariants was shown to be NP-hard in [19]. These studies differ primarily in the types of invariants considered: linear invariants in [20], a single quadratic polynomial in [8], and pure difference binomials in [7]. In contrast, [9] considers general polynomial invariants but lacks completeness guarantees and does not address guard conditions.
Higher-degree loops have been investigated in a more general framework in [21], which also considers polynomial inequalities as input. However, the loops synthesized by that algorithm are restricted to cases where the input invariants are inductive, that is if an invariant holds after one iteration, it continues to hold for all subsequent iterations.

**Our contributions.** In this work, we consider the following situation: the generation of polynomial loops with guards from arbitrary polynomial invariants (equalities). We take the first step towards this goal by generating a polynomial system whose solutions correspond exactly to loops with a given structure that satisfy the specified polynomial invariants. We then discuss different strategies that can be used to solve this system. In practice, in most cases a satisfying solution is found using an SMT solver.

More precisely, in Section 2 we recall the definition of invariant sets and relevant results from [22]. Section 3 introduces a method for simultaneously identifying multiple polynomial invariants (Proposition 3) and applies it to show that the set $C(\mathbf{a}, \mathbf{h}, \mathbf{f}; \mathbf{g})$, the collection of all coefficients of polynomial maps of loops satisfying the polynomial invariants $\mathbf{g}$ with respect to $\mathbf{f}$, forms an algebraic variety. We also present Algorithm 2, which computes the defining polynomials of $C(\mathbf{a}, \mathbf{h}, \mathbf{f}; \mathbf{g})$. Section 4 discusses several strategies for solving the resulting polynomial systems and highlights their limitations. Finally, in Section 5 we describe our implementation of the algorithms and report the experimental results.

**Extended version.** This paper is an extended version of the paper [23], published in the Proceedings of the 14th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis. It expands on the earlier work by providing extended results and introducing new contributions. Specifically, Section 3.2 generalizes our previous work by addressing branching loops with nondeterministic conditional statements, whereas the earlier paper focused only on single-path loops. Section 3.3 introduces a new class of invariants, and we develop Algorithm 3 to compute polynomial equations that characterize all branching loops with a given structure that satisfy these invariants. In contrast to Algorithm 2, Algorithm 3 avoids costly Gröbner basis computation. In addition, when the given invariants are affine, Proposition 8 shows that the set of coefficients of the update map for a loop satisfying these invariants forms an affine space. Algorithm 4 is then used to compute an affine basis for this space.

## 2 Preliminaries

Here, we introduce the main objects of this paper and extend key results from [22, 10].

### 2.1 Invariant sets for a single polynomial map

**Definition 5** Let $F: \mathbb{C}^n \to \mathbb{C}^n$ be a polynomial map and $X \subset \mathbb{C}^n$. The invariant set of $(F, X)$ is defined as:

$$S_{(F,X)} = \{x \in X \mid \forall m \in \mathbb{N}, F^{(m)}(x) \in X\}.$$

The following proposition, adapted from [22, Proposition 2.3], is the key result enabling the invariant sets to be computed algebraically.

**Proposition 1** Let $X \subseteq \mathbb{C}^n$ be an algebraic variety and consider a polynomial map $F: \mathbb{C}^n \to \mathbb{C}^n$. We define

$$X_m = X \cap F^{-1}(X) \cap \dots \cap F^{-m}(X)$$

for all $m \in \mathbb{N}$. Then, there exists $N \in \mathbb{N}$ such that $X_N = X_{N+1}$, and for any such index $X_N = S_{(F,X)}$.

Building on Proposition 1, the following algorithm computes invariant sets by means of an iterative outer approximation that converges in finitely many steps. The algorithm requires the following procedures:

- **Compose**: given two sequences of polynomials $\mathbf{g} = (g_1, \dots, g_m)$ and $F = (F_1, \dots, F_n)$ in $\mathbb{Q}[\mathbf{x}]$, it returns $g_1(F_1(\mathbf{x}), \dots, F_n(\mathbf{x})), \dots, g_m(F_1(\mathbf{x}), \dots, F_n(\mathbf{x}))$.

- **InRadical**: given a sequence of polynomials $\tilde{\mathbf{g}}$ and a finite set $S \subset \mathbb{Q}[\mathbf{x}]$, it outputs True if $\tilde{\mathbf{g}} \subset \sqrt{\langle S \rangle}$, and False otherwise.

These procedures are standard routines in symbolic computation and the latter one can be carried out efficiently using techniques such as Gröbner bases [3]. For further details, we refer the reader to [10].

**Algorithm 1 InvariantSet**

**Input:** sequences $\mathbf{g}$ and $F = (F_1, \dots, F_n)$ in $\mathbb{Q}[\mathbf{x}]$.

**Output:** polynomials of common zero-set $S_{(F,V(\mathbf{g}))}$.

1: $S \leftarrow \{\mathbf{g}\}$;

2: $\tilde{\mathbf{g}} \leftarrow \text{Compose}(\mathbf{g}, F)$;

3: **while** $\text{InRadical}(\tilde{\mathbf{g}}, S) == \text{False}$ **do**

4: $S \leftarrow S \cup \{\tilde{\mathbf{g}}\}$;

5: $\tilde{\mathbf{g}} \leftarrow \text{Compose}(\tilde{\mathbf{g}}, F)$;

6: **end while**

7: **return** $S$;

The termination and correctness of Algorithm 1 follow from Proposition 1 and [22, Theorem 2.4].
**Example 1** Consider the polynomial map and the algebraic variety:

$F = (2x_1 - 3x_2, x_1 + x_2)$ and $X = V(x_1^2 - x_2^2 + x_1x_2)$,

respectively. On input $F$ and $g = x_1^2 - x_2^2 + x_1x_2$, Algorithm 1 computes the invariant set of $(F, X)$ through the following steps:

- At Step 1, $S \leftarrow \{g\}$. At Step 2, $\tilde{g}$ is set to

$$ \text{Compose}(g, F) = 5x_1^2 - 15x_1x_2 + 5x_2^2. $$

- At Step 3, a Gröbner basis of the ideal $\langle g, 1 - t\tilde{g} \rangle$ is computed which makes the following decision

$$ \text{InRadical}(\tilde{g}, S) = \text{False}. $$

- At Step 4, $S \leftarrow \{g, g \circ F\}$. At Step 5, $\tilde{g}$ is updated as

$$ \text{Compose}(\tilde{g}, F) = -5x_1^2 - 35x_1x_2 + 95x_2^2. $$

- This time, $\text{InRadical}(\tilde{g}, S) = \text{True}$, so the while-loop terminates.

Therefore, the invariant set is $S_{(F, V(g))} = V(g, g \circ F)$.

## 2.2 Invariants sets for multiple polynomial loops

In many cases, we are interested not in a single polynomial loop but in systems with multiple loops or updates. This subsection generalizes the notion of invariant sets to the setting of multiple polynomial loops.

**Definition 6** Let $F_1, \dots, F_k : \mathbb{C}^n \to \mathbb{C}^n$ be polynomial maps. For any $m \in \mathbb{N}$ and any sequence $i_1, \dots, i_m \in [k]$, define the polynomial map

$$ F_{i_1, \dots, i_m}(\mathbf{x}) = F_{i_m}(F_{i_{m-1}}(\dots F_{i_1}(\mathbf{x}))). $$

The next definition extends Definition 5 to the setting of multiple polynomial maps.

**Definition 7** Consider the set $X \subseteq \mathbb{C}^n$ and the polynomial maps $F_1, \dots, F_k : \mathbb{C}^n \to \mathbb{C}^n$. The invariant set of $(F_1, \dots, F_k), X)$ is defined as

$$ \{x \in X \mid \forall m \ge 1, \forall i_1, \dots, \forall i_m \in [k], F_{i_m}(\dots(F_{i_1}(x)) \in X\} $$
where $[k] = \{1, \dots, k\}$. We note it $S_{((F_1, \dots, F_k), X)}$.

The next proposition introduce an algorithm for computing invariant sets of multiple polynomial maps. For more details, this is an adaptation of in [10, Theorem 3.14].

**Proposition 2** Let $F_1, \dots, F_k$ and $g$ be sequences of polynomial in $\mathbb{Q}[\mathbf{x}]$. Define $\text{InvariantSetBranch}$ the modified version of Algorithm 1, obtained by replacing

- **Compose(g, F)** with the tuple
  $((\text{Compose}(g, F_1), \dots, \text{Compose}(g, F_k))$

in Step 2; and

- **Compose(\tilde{g}, F)** with the tuple
  $(\text{Compose}(\tilde{g}, F_1), \dots, \text{Compose}(\tilde{g}, F_k))$

in Step 5.

Then, on input the $F_i$ and $g$, $\text{InvariantSetBranch}$ computes polynomials whose common zero-set is the invariant set of $((F_1, \dots, F_k), V(g))$.

## 3 From loops to polynomial systems

In this section, we present a method for identifying all (branching) loops that satisfy given polynomial invariants by formulating the problem as a polynomial system over invariant sets. This reduces loop synthesis to solving a polynomial system, which will be examined in detail in the next section.

### 3.1 Single-path loops

We first consider single-path loops, i.e. loops defined by a single polynomial update map $F : \mathbb{C}^n \to \mathbb{C}^n$ with an inequality $h(x) \neq 0$ in the guard condition. This case provides the basic setting in which to study invariant sets, before extending the results to branching loops in Section 3.2.

The following lemma, which is an immediate consequence of Definition 5, shows that invariant sets are preserved under intersections of algebraic varieties.

**Lemma 1** Let $F : \mathbb{C}^n \to \mathbb{C}^n$ be a polynomial map, and let $X_1, \dots, X_m \subseteq \mathbb{C}^n$ be algebraic varieties. Then

$$ S_{(F, X_1 \cap \dots \cap X_m)} = S_{(F, X_1)} \cap \dots \cap S_{(F, X_m)}. $$

We now provide a necessary and sufficient condition for determining whether a given set of polynomials forms invariants of a loop. Furthermore, the next proposition extends [10, Proposition 2.7], where the statement was established for a single polynomial invariant.

**Proposition 3** Let $h, g_1, \dots, g_m \in \mathbb{C}[\mathbf{x}]$, and let $z$ be a new indeterminate. Define

$$ X = V(zg_1, \dots, zg_m) \subset \mathbb{C}^{n+1}. $$

Let $F : \mathbb{C}^n \to \mathbb{C}^n$ be a polynomial map, and define

$$ G_h(\mathbf{x}, z) = (F(\mathbf{x}), zh(\mathbf{x})). $$

Then, for $\mathbf{a} \in \mathbb{C}^n$, one has $\mathbf{g} \subseteq I_{\mathcal{L}(\mathbf{a}, h, F)}$ if and only if $(\mathbf{a}, 1) \in S_{(G_h, X)}$.
**Proof** For each $i \in \{1, \dots, m\}$, let $X_i = \mathbf{V}(zg_i) \subset \mathbb{C}^{n+1}$ be an algebraic variety. By [10, Proposition 2.7], we have

$$g_i \in I_{\mathcal{L}(\mathbf{a},h,F)} \iff (\mathbf{a}, 1) \in S_{(G_h, X_i)}.$$

Hence, $g_1, \dots, g_m \in I_{\mathcal{L}(\mathbf{a},h,F)}$ if and only if

$$(\mathbf{a}, 1) \in S_{(G_h, X_1)} \cap \dots \cap S_{(G_h, X_m)}.$$

By Lemma 1, it follows that

$$S_{(G_h, X)} = S_{(G_h, X_1)} \cap \dots \cap S_{(G_h, X_m)}.$$

Hence, $g_1, \dots, g_m \in I_{\mathcal{L}(\mathbf{a},h,F)}$ if and only if $(\mathbf{a}, 1) \in S_{(G_h, X)}$. $\square$

The next proposition provides a necessary and sufficient condition for loops with a given structure to satisfy specified polynomial invariants.

**Proposition 4** Let $\mathbf{f}_i = (f_{i,1}, \dots, f_{i,l_i})$ be a sequence of polynomials in $\mathbb{C}[\mathbf{x}]$ for every $i \le n$, and define $\mathbf{f} = (\mathbf{f}_1, \dots, \mathbf{f}_n)$. Let $z, y_{i,1}, \dots, y_{i,l_i}$ be new indeterminates for every $i \le n$, and let $h \in \mathbb{C}[\mathbf{x}]$. Let $H_h$ be the map

$$\mathbb{C}^{n+\sum_{j=1}^n l_j+1} \to \mathbb{C}^{n+\sum_{j=1}^n l_j+1} \\ (\mathbf{x}, \mathbf{y}, z) \mapsto \left( \sum_{i=1}^{l_1} y_{1,i} f_{1,i}(\mathbf{x}), \dots, \sum_{i=1}^{l_n} y_{n,i} f_{n,i}(\mathbf{x}), \mathbf{y}, zh(\mathbf{x}) \right).$$

Let $\mathbf{g} = (g_1, \dots, g_m)$ be a sequence of polynomials in $\mathbb{C}[\mathbf{x}]$, viewed as elements of $\mathbb{C}[\mathbf{x}, \mathbf{y}, z]$, and define

$$X = \mathbf{V}(zg_1, \dots, zg_m) \subset \mathbb{C}^{n+\sum_{j=1}^n l_j+1}.$$

Then, for any $\mathbf{a} \in \mathbb{C}^n$,

$$\mathcal{C}(\mathbf{a}, h, \mathbf{f}; \mathbf{g}) = \{ \mathbf{b} \in \mathbb{C}^{\sum_{j=1}^n l_j} \mid (\mathbf{a}, \mathbf{b}, 1) \in S_{(H_h, X)} \}.$$

*Proof* Write $H_h(\mathbf{x}, \mathbf{y}, z) = (H(\mathbf{x}, \mathbf{y}), zh(\mathbf{x}))$, where

$$H(\mathbf{x}, \mathbf{y}) = \left( \sum_{i=1}^{l_1} y_{1,i} f_{1,i}(\mathbf{x}), \dots, \sum_{i=1}^{l_n} y_{n,i} f_{n,i}(\mathbf{x}), \mathbf{y} \right).$$

By Proposition 3, $g_1, \dots, g_m$ are polynomial invariants of $\mathcal{L}((\mathbf{a}, \mathbf{b}), h, H)$ if and only if $(\mathbf{a}, \mathbf{b}, 1)$ is contained in $S_{(H_h, X)}$. Since the value of $\mathbf{y}$ remains fixed at $\mathbf{b}$ under iteration, for all $N \in \mathbb{N}$, we have

$$H^N(\mathbf{x}, \mathbf{b}) = (F_{\mathbf{f},\mathbf{b}}^N(\mathbf{x}), \mathbf{b}).$$

Hence, $\mathbf{g} \subset I_{\mathcal{L}(\mathbf{a},h,F_{\mathbf{f},\mathbf{b}})}$ if and only if $\mathbf{g} \subset I_{\mathcal{L}((\mathbf{a}, \mathbf{b}),h,H)}$, which in turn holds if and only if $(\mathbf{a}, \mathbf{b}, 1) \in S_{(H_h, X)}$. $\square$

Since the invariant set is an algebraic variety, Proposition 4 implies that $\mathcal{C}(\mathbf{a}, h, \mathbf{f}; \mathbf{g})$ is likewise an algebraic variety. Its defining equations are obtained by substituting $\mathbf{x} = \mathbf{a}$ and $z = 1$ into the system that defines the invariant set.

The following algorithm computes a generating set of polynomials for $\mathcal{C}(\mathbf{a}, h, \mathbf{f}; \mathbf{g})$.

**Algorithm 2 GenerateLoops**

**Input:** $h, g_1, \dots, g_m, f_{1,1}, \dots, f_{1,l_1}, \dots, f_{n,1}, \dots, f_{n,l_n}$ in $\mathbb{Q}[\mathbf{x}]$ and $\mathbf{a} \in \mathbb{Q}^n$.
**Output:** A set of polynomials $\{P_1, \dots, P_s\}$ such that $\mathcal{C}(\mathbf{a}, h, \mathbf{f}; \mathbf{g})$ is $\mathbf{V}(P_1, \dots, P_s)$

1: $H_h \leftarrow \left( \sum_{i=1}^{l_1} y_{1,i} f_{1,i}(\mathbf{x}), \dots, \sum_{i=1}^{l_n} y_{n,i} f_{n,i}(\mathbf{x}), \mathbf{y}, zh(\mathbf{x}) \right)$

2: $\{Q_1, \dots, Q_s\} \leftarrow \text{InvariantSet}((zg_1, \dots, zg_m), H_h)$;

3: $\{P_1(\mathbf{y}), \dots, P_s(\mathbf{y})\} \leftarrow \{Q_1(\mathbf{a}, \mathbf{y}, 1), \dots, Q_s(\mathbf{a}, \mathbf{y}, 1)\}$

4: **return** $\{P_1, \dots, P_s\}$;

**Theorem 1** Let $\mathbf{a} \in \mathbb{Q}^n$, $h \in \mathbb{C}[\mathbf{x}]$, $\mathbf{g} = (g_1, \dots, g_m)$, and $\mathbf{f}_1 = (f_{1,1}, \dots, f_{1,l_1}), \dots, \mathbf{f}_n = (f_{n,1}, \dots, f_{n,l_n})$ be sequences of polynomials in $\mathbb{Q}[\mathbf{x}]$. Set $\mathbf{f} = (\mathbf{f}_1, \dots, \mathbf{f}_n)$. Given input $(\mathbf{a}, h, \mathbf{f}, \mathbf{g})$, Algorithm 2 outputs a set of polynomials whose vanishing locus is $\mathcal{C}(\mathbf{a}, h, \mathbf{f}; \mathbf{g})$.

**Proof** We prove the correctness of Algorithm 2. Let $X = \mathbf{V}(zg_1, \dots, zg_m) \subset \mathbb{C}^{n+l_1+\dots+l_n+1}$. At Step 2, by [22, Theorem 2.4], InvariantSet outputs

$$\{Q_1(\mathbf{x}, \mathbf{y}, z), \dots, Q_s(\mathbf{x}, \mathbf{y}, z)\},$$

such that $S_{(H_h, X)}$ is the common zero-set of $\{Q_1, \dots, Q_s\}$. Hence, by Proposition 4, $g_1, \dots, g_m$ are polynomial invariants of $\mathcal{L}(\mathbf{a}, h, F_{\mathbf{f},\mathbf{b}})$ if and only if

$$Q_1(\mathbf{a}, \mathbf{b}, 1) = \dots = Q_s(\mathbf{a}, \mathbf{b}, 1) = 0.$$

Consequently, $g_1, \dots, g_m \in I_{\mathcal{L}(\mathbf{a},h,F_{\mathbf{f},\mathbf{b}})}$ if and only if

$$P_1(\mathbf{b}) = \dots = P_s(\mathbf{b}) = 0,$$

which establishes the correctness of Algorithm 2. $\square$

In the examples below, to distinguish program variables from the coefficients of the update maps, we denote the coefficients by $\lambda$ instead of $y$.

**Example 2** Consider the polynomial map

$$F(x_1, x_2, x_3) = (\lambda_1 x_1^3 + \lambda_2 x_2^2, \lambda_3 x_1 + \lambda_4 x_2^2, \lambda_5 x_1),$$

and the polynomial invariants $g_1 = x_2^2 - x_1$ and $g_2 = x_3^3 + 2x_2^2 - x_1$. Our goal is to determine all loops of
this form with precondition $(x_1, x_2, x_3) = (1, 1, -1)$ and postcondition $(x_2^2 - x_1 = 0, x_3^3 + 2x_2^2 - x_1 = 0)$:

$$ (x_1, x_2, x_3) \leftarrow (1, 1, -1) $$

while true do

$$ \begin{pmatrix} x_1 \\ x_2 \\ x_3 \end{pmatrix} \leftarrow F \begin{pmatrix} \lambda_1 x_1^3 + \lambda_2 x_2^2 \\ \lambda_3 x_1 + \lambda_4 x_2^2 \\ \lambda_5 x_1 \end{pmatrix} $$

end while

Let $F = (F_1, F_2, F_3)$ and $g = \{g_1, g_2\}$, and define

$$ f = \{\{x_1^3, x_2^2\}, \{x_1, x_2^2\}, \{x_1\}\}. $$

From the loop structure we have

$$ F_1 \in \operatorname{span}\{x_1^3, x_2^2\}, \quad F_2 \in \operatorname{span}\{x_1, x_2^2\}, \quad F_3 \in \operatorname{span}\{x_1\}. $$

Thus, the input to Algorithm 2 is $(\{1\}, g, f, \{1, 1, -1\})$. Let $X = V(\{zg_1, zg_2\}) \subset \mathbb{C}^9$ and define the map

$$ H_h(\mathbf{x}, \mathbf{y}, z) = (y_1 x_1^3 + y_2 x_2^2, y_3 x_1 + y_4 x_2^2, y_5 x_1, \mathbf{y}, z). $$

At Step 2, given input $H_h$ and $X$, InvariantSet outputs polynomials

$$ \{Q_1(\mathbf{x}, \mathbf{y}, z), \dots, Q_6(\mathbf{x}, \mathbf{y}, z)\}. $$

whose vanishing locus is the invariant set $S_{(H_h,X)}$. Substituting the initial values of the loop into these polynomials yields four nonzero polynomials $P_1(\mathbf{y}), \dots, P_4(\mathbf{y})$, whose vanishing locus is $\mathscr{C}((1, 1, -1), 1, f; g)$:

$$ \begin{align*} P_1 &= (y_3 + y_4)^2 - y_1 - y_2, & P_2 &= y_5^3 + 2(y_3 + y_4)^2 - y_1 - y_2, \\ P_3 &= 2y_3^4 y_4^2 + 8y_3^3 y_4^3 + 12y_3^2 y_4^4 + 8y_3 y_4^5 + 2y_4^6 + y_3^3 y_5^3 + \\ & 3y_1^2 y_2 y_5^3 + 3y_1 y_2^2 y_3^3 + y_3^2 y_5^3 + 4y_1 y_3^3 y_4 + 4y_2 y_3^3 y_4 + 8y_1 y_3^2 y_4^2 + \\ & 8y_2 y_3^2 y_4^2 + 4y_1 y_3 y_4^3 + 4y_2 y_3 y_4^3 - y_1^4 - 3y_3^3 y_2 - 3y_1^2 y_2^2 - \\ & y_1 y_3^2 + 2y_1^2 y_3^2 + 4y_1 y_2 y_3^2 + 2y_2^2 y_3^2 - y_2 y_3^2 - 2y_2 y_3 y_4 - y_2 y_4^2, \\ P_4 &= y_3^4 y_4^2 + 4y_3^3 y_4^3 + 6y_3^2 y_4^4 + 4y_3 y_4^5 + y_4^6 + 2y_1 y_3^3 y_4 + 2y_2 y_3^3 y_4 + \\ & 4y_1 y_3^2 y_4^2 + 4y_2 y_3^2 y_4^2 + 2y_1 y_3 y_4^3 + 2y_2 y_3 y_4^3 - y_1^4 - 3y_3^3 y_2 - \\ & 3y_1^2 y_2^2 - y_1 y_2^3 + y_1^2 y_3^2 + 2y_1 y_2 y_3^2 + y_2^2 y_3^2 - y_2 y_3^2 - 2y_2 y_3 y_4 - y_2 y_4^2. \end{align*} $$

**Remark 1** This algorithm can be straightforwardly extended to select an initial value in addition to the update map of the loop. Indeed, when no initial values are specified, Step 2 of Algorithm 2 produces a sequence of polynomials

$$ (Q_1, \dots, Q_s) \subset \mathbb{Q}[\mathbf{x}, \mathbf{y}, z] $$

such that $\mathbf{b} \in \mathscr{C}(\mathbf{a}, h, f; g)$ if and only if

$$ Q_1(\mathbf{a}, \mathbf{b}, 1) = \dots = Q_s(\mathbf{a}, \mathbf{b}, 1) = 0. $$

Consequently, Algorithm 2 applies even in the absence of initial values.

## 3.2 Generalization to branching loops

In this section, we extend the results on single-path loops to branching loops $\mathcal{L}(\mathbf{a}, h, (F_1, \dots, F_k))$, which are defined by a nondeterministic conditional statement with $k$ branches:

$$ (x_1, \dots, x_n) := (a_1, \dots, a_n) $$

while $h \neq 0$ do

if $*$ then

$$ (x_1, \dots, x_n) \leftarrow F_1(x_1, \dots, x_n) $$

⋮

else if $*$ then

$$ (x_1, \dots, x_n) \leftarrow F_i(x_1, \dots, x_n) $$

⋮

else

$$ (x_1, \dots, x_n) \leftarrow F_k(x_1, \dots, x_n) $$

end if

end while

Here $\mathbf{a} = (a_1, \dots, a_n) \in \mathbb{C}^n, h \in \mathbb{C}[\mathbf{x}]$, and

$$ F_1, \dots, F_k : \mathbb{C}^n \to \mathbb{C}^n $$

are polynomial maps. When no guard $h$ is specified, we simply write $\mathcal{L}(\mathbf{a}, 1, (F_1, \dots, F_k))$.

The following lemma, an immediate consequence of Definition 7, shows that invariant sets remain closed under intersections in the branching case.

**Lemma 2** Let $F_1, \dots, F_k : \mathbb{C}^n \to \mathbb{C}^n$ be polynomial maps and let $X_1, \dots, X_m \subseteq \mathbb{C}^n$ be algebraic varieties. Denote $\mathbf{F} = (F_1, \dots, F_k)$. Then

$$ S(\mathbf{F}, X_1 \cap \dots \cap X_m) = S(\mathbf{F}, X_1) \cap \dots \cap S(\mathbf{F}, X_m). $$

The invariant ideal $I_{\mathcal{L}(\mathbf{a},h,(F_1,\dots,F_k))}$ of a branching loop is defined in [10, Definition 3.11] as the set of all polynomial invariants of the loop. The following proposition extends Proposition 3; the proof is the same, except that [10, Proposition 3.15] is invoked in place of [10, Proposition 2.7].

**Proposition 5** Let $F_1, \dots, F_k : \mathbb{C}^n \to \mathbb{C}^n$ be polynomial maps and let $h, g_1, \dots, g_m \in \mathbb{C}[\mathbf{x}]$. Let $z$ be a new indeterminate, and define the variety

$$ X = V(\{zg_1, \dots, zg_m\}) \subset \mathbb{C}^{n+1}. $$

For each $i \le k$, define the polynomial map

$$ G_{i,h}(\mathbf{x}, z) = (F_i(\mathbf{x}), zh(\mathbf{x})). $$

Then

$$ g \subseteq I_{\mathcal{L}(\mathbf{a},h,(F_1,\dots,F_k))} \iff (\mathbf{a}, 1) \in S((G_{1,h},\dots,G_{k,h}),X). $$
We now define the set of branching loops, specified by multiple polynomial maps, an initial value, and a guard condition, that satisfy a given collection of polynomial invariants. The following definition extends Definition 4.

**Definition 8** For each $i \le k$ and $j \le n$, let $\mathbf{f}_{i,j} = (f_{i,j,1}, \dots, f_{i,j,n_{i,j}})$ be a sequence of polynomials in $\mathbb{C}[\mathbf{x}]$ and let $h \in \mathbb{C}[\mathbf{x}]$. Let $\mathbf{g} = (g_1, \dots, g_m)$ be a sequence of polynomials in $\mathbb{C}[\mathbf{x}]$, and set $\mathbf{f}_i = (\mathbf{f}_{i,1}, \dots, \mathbf{f}_{i,n})$ for each $i \le k$.

The set of branching loops structured by $(\mathbf{f}_1, \dots, \mathbf{f}_k)$ and satisfying the invariants $\mathbf{g}$ is the coefficient set $\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$ defined by

$$ \{(\mathbf{a}, \mathbf{b}_1, \dots, \mathbf{b}_k) \in \mathbb{C}^M \mid \mathbf{g} \subseteq I_{\mathcal{L}(\mathbf{a},h,(F_{\mathbf{f}_1,\mathbf{b}_1}, \dots, F_{\mathbf{f}_k,\mathbf{b}_k}))}\}, $$
where $M = n + \sum_{i=1}^k \sum_{j=1}^n n_{i,j}$.

Thus, $\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$ consists of all choices of initial values and coefficients that yield branching loops satisfying the polynomial invariants $\mathbf{g}$.

Hence, to synthesize a branching loop structured by $(\mathbf{f}_1, \dots, \mathbf{f}_k)$ that satisfies $\mathbf{g}$, it suffices to identify a vector in $\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$.

We now show that $\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$ is an invariant set, analogous to Proposition 4 for the single-map case. The proof is similar and therefore omitted.

**Proposition 6** *Using the notation of Definition 8, let $z$ and $y_{i,j,l}$ be new indeterminates for every $i \le k$, $j \le n$, and $l \le n_{i,j}$. For each $i \le k$, define the polynomial map $H_{i,h} : \mathbb{C}^{M+1} \to \mathbb{C}^{M+1}$ in $\mathbb{C}[\mathbf{x}, \mathbf{y}, z]$ such that $H_{i,h}(\mathbf{x}, \mathbf{y}, z)$ is equal to*

$$ \left( \sum_{l=1}^{n_{i,1}} y_{i,1,l} f_{i,1,l}(\mathbf{x}), \dots, \sum_{l=1}^{n_{i,n}} y_{i,n,l} f_{i,n,l}(\mathbf{x}), \mathbf{y}, zh(\mathbf{x}) \right). $$

Define $X = \mathbf{V}(zg_1, \dots, zg_m) \subset \mathbb{C}^{M+1}$, and set $\mathbf{b} = (\mathbf{b}_1, \dots, \mathbf{b}_k)$. Then $\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$ is the set

$$ \{(\mathbf{a}, \mathbf{b}) \in \mathbb{C}^M \mid (\mathbf{a}, \mathbf{b}, 1) \in S_{((H_{1,h}, \dots, H_{k,h}), X)}\}. $$

Therefore, by computing a defining set of polynomials for the invariant set $S_{((H_{1,h}, \dots, H_{k,h}), X)}$ and then substituting $z = 1$, we obtain defining equations for $\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$. An algorithm for computing these equations in the branching (multi-map) setting is provided by Proposition 2. The following example illustrates the procedure step by step, yielding a defining set of polynomials for $\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$.

**Example 3** Consider branching loops with a nondeterministic conditional statement involving two branches, given by

$$ F_1(x_1, x_2) = (\lambda_1 x_1 + \lambda_2, \lambda_3 x_2), $$

$$ F_2(x_1, x_2) = (\lambda_4 x_2 + \lambda_5, \lambda_6 x_1), $$

that satisfy the polynomial invariant $g = 2x_1 - x_2^2$. Hence, we aim to compute all branching loops of the following form that preserve $g$:

$$ \begin{array}{l} (x_1, x_2) := (a_1, a_2) \\ \textbf{while} \ 1 \neq 0 \ \mathbf{do} \\ \quad \mathbf{if} \ \ast \ \mathbf{then} \\ \quad \quad (x_1, x_2) \leftarrow F_1 \quad (\lambda_1 x_1 + \lambda_2, \lambda_3 x_2) \\ \quad \mathbf{else} \\ \quad \quad (x_1, x_2) \leftarrow F_2 \quad (\lambda_4 x_2 + \lambda_5, \lambda_6 x_1) \\ \quad \mathbf{end} \ \mathbf{if} \\ \quad \mathbf{end} \ \mathbf{while} \end{array} $$

Let $\mathbf{f}_1 = \{(x_1, 1), \{x_2\}\}$ and $\mathbf{f}_2 = \{\{x_2, 1\}, \{x_1\}\}$. Then $\mathcal{L}((a_1, a_2), 1, (F_1, F_2))$ satisfies the polynomial invariant $g$ if and only if

$$ (a_1, a_2, \lambda_1, \dots, \lambda_6) \in \mathcal{C}(1, (\mathbf{f}_1, \mathbf{f}_2), g). $$

Let $X = \mathbf{V}(zg) \subset \mathbb{C}^9$, and define the polynomial maps

$$ H_{1,h}(\mathbf{x}, \mathbf{y}, z) = (y_1 x_1 + y_2, y_3 x_2, \mathbf{y}, z), $$

$$ H_{2,h}(\mathbf{x}, \mathbf{y}, z) = (y_4 x_2 + y_5, y_6 x_1, \mathbf{y}, z). $$

By Proposition 6, $(a_1, a_2, \lambda_1, \dots, \lambda_6) \in \mathcal{C}(1, (\mathbf{f}_1, \mathbf{f}_2), g)$ if and only if $(a_1, a_2, \lambda_1, \dots, \lambda_6, 1) \in S_{(H_{1,h}, H_{2,h}), X}$. On input $H_{1,h}$, $H_{2,h}$ and $X$, InvariantSetBranch outputs 31 polynomials

$$ \{Q_1(\mathbf{x}, \mathbf{y}, z), \dots, Q_{31}(\mathbf{x}, \mathbf{y}, z)\}, $$

whose vanishing locus is $S_{(H_{1,h}, H_{2,h}), X}$. Therefore, the vanishing locus of the equations

$$ Q_1(\mathbf{x}, \mathbf{y}, 1) = 0, \dots, Q_{31}(\mathbf{x}, \mathbf{y}, 1) = 0, $$

is $\mathcal{C}(1, (\mathbf{f}_1, \mathbf{f}_2), g)$. Below we present six sample polynomials among these:

$$ \begin{aligned} & 2x_1 - x_2^2; \quad 2y_1x_1 + 2y_2 - y_3^2x_2^2; \quad 2y_4x_2 + 2y_5 - y_6^2x_1^2; \\ & 2y_1^2x_1 + 2y_1y_2 + 2y_2 - y_3^4x_2^2; \quad 2y_1y_4x_2 + 2y_1y_5 + 2y_2 - y_3^2y_6^2x_1^2 \\ & -y_1^2y_6^2x_1^2 - 2y_1y_2y_6^2x_1 - y_2^2y_6^2 + 2y_3y_4x_2 + 2y_5. \end{aligned} $$

**Remark 2** Similarly to Remark 1, we can extend this approach (and in particular the previous algorithm) to also synthesize guard inequations. Indeed, using the notation of Definition 8, let $z$, $y_{i,j,l}$ and $w_1, \dots, w_r$ be new indeterminates for every $i \le k$, $j \le n$, and $l \le n_{i,j}$. Let $h = (h_1, \dots, h_r)$ be a sequence of polynomials in $\mathbb{Q}[\mathbf{x}]$ given as input. We look for guard polynomial is of the form

$$ h(\mathbf{x}, \mathbf{w}) = w_1 h_1(\mathbf{x}) + \dots + w_r h_r(\mathbf{x}) $$

where $\mathbf{w} = (w_1, \dots, w_r)$. For each $i \le k$, define polynomial maps $H_{i,h}(\mathbf{x}, \mathbf{y}, z, \mathbf{w})$
$$ \left( \sum_{l=1}^{n_{i,1}} y_{i,1,l} f_{i,1,l}(\mathbf{x}), \dots, \sum_{l=1}^{n_{i,n}} y_{i,n,l} f_{i,n,l}(\mathbf{x}), \mathbf{y}, zh(\mathbf{x}, \mathbf{w}), \mathbf{w} \right). $$

Define $X = \mathbf{V}(zg_1, \dots, zg_m)$. By computing defining equations for the invariant set

$$ S((H_{1,h}, \dots, H_{k,h}), X) $$

and then substituting $z = 1$, we obtain equations

$$ P_1(\mathbf{x}, \mathbf{y}, \mathbf{w}) = 0, \dots, P_s(\mathbf{x}, \mathbf{y}, \mathbf{w}) = 0 $$

such that $(\mathbf{a}, \mathbf{b})$ is contained in $\mathcal{C}(h(\mathbf{x}, \mathbf{c}), (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g})$ if and only if $P_1(\mathbf{a}, \mathbf{b}, \mathbf{c}) = \dots = P_s(\mathbf{a}, \mathbf{b}, \mathbf{c}) = 0$.

### 3.3 Universally inductive invariants

Algorithm 2 relies on Gröbner basis computation, whose worst case complexity can be doubly exponential in the number of variables [24]. Consequently, when the template of the update map contains many generators, Algorithm 2 may fail to terminate within a reasonable time. Moreover, the degrees of the polynomial equations computed by Algorithm 2 can grow exponentially.

In this subsection, we address these issues by focusing on a special class of invariants. For this class, we rely only on linear algebra to generate polynomial equations characterizing loops that satisfy the given invariants, and the degrees of these equations are bounded above by the degrees of the invariants themselves.

#### 3.3.1 General case

In this subsection, we consider polynomial invariants of the form $g(\mathbf{x}) - g(\mathbf{a})$, which hold for every initial value $\mathbf{a} \in \mathbb{C}^n$. Equivalently, $g(\mathbf{x}) - g(\mathbf{a})$ is an invariant of $\mathcal{L}(\mathbf{a}, h, (F_1, \dots, F_k))$ for all $\mathbf{a} \in \mathbb{C}^n$.

**Definition 9** Let $F_1, \dots, F_k: \mathbb{C}^n \to \mathbb{C}^n$ be polynomial maps, and let $h \in \mathbb{C}[\mathbf{x}]$. A polynomial $g(\mathbf{x})$ is called a universally inductive invariant of $\mathcal{L}(h, (F_1, \dots, F_k))$ if $g(\mathbf{x}) - g(\mathbf{a})$ is an invariant of $\mathcal{L}(\mathbf{a}, h, (F_1, \dots, F_k))$ for every $\mathbf{a} \in \mathbb{C}^n$. The set of all universally inductive invariants of $\mathcal{L}(h, (F_1, \dots, F_k))$ is denoted by $UI_{\mathcal{L}(h, (F_1, \dots, F_k))}$.

We now define the coefficient set that characterizes all branching loops structured by $(\mathbf{f}_1, \dots, \mathbf{f}_k)$ which satisfies a prescribed collection of universally inductive invariants.

**Definition 10** Using the notation of Definition 8, the set of all branching loops structured by $(\mathbf{f}_1, \dots, \mathbf{f}_k)$ that satisfy the universally inductive invariants $g$ is defined by the coefficient set $\mathcal{U}\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); g)$, which is

$$ \left\{ (\mathbf{b}_1, \dots, \mathbf{b}_k) \in \mathbb{C}^M \mid \mathbf{g} \subseteq UI_{\mathcal{L}(h, (\mathbf{F}_{\mathbf{f}_1}, \mathbf{b}_1, \dots, \mathbf{F}_{\mathbf{f}_k}, \mathbf{b}_k))} \right\}, $$

where $M = \sum_{i=1}^k \sum_{j=1}^n n_{i,j}$.

The following proposition, stated in [10, Corollary 4.4], provides a necessary and sufficient condition for a polynomial to be a universally inductive invariant. For completeness, we include a brief proof.

**Proposition 7** Let $F_1, \dots, F_k: \mathbb{C}^n \to \mathbb{C}^n$ be polynomial maps, and let $h(\mathbf{x}) \in \mathbb{C}[\mathbf{x}]\setminus\{0\}$. Then a polynomial $g(\mathbf{x})$ is a universally inductive invariant if and only if

$$ g(F_i(\mathbf{x})) = g(\mathbf{x}) \quad \text{for every } i \le k. $$

*Proof* (⇒) Suppose $g$ is a universally inductive invariant. Let $\mathbf{a} \notin \mathbf{V}(h)$. By the definition of invariant polynomials,

$$ g(F_i(\mathbf{a})) - g(\mathbf{a}) = 0 $$

for every $i \le k$. Hence $g(F_i(\mathbf{a})) = g(\mathbf{a})$ for all $\mathbf{a} \notin \mathbf{V}(h)$. Now let $\mathbf{a} \in \mathbf{V}(h)$. Since $h(\mathbf{x}) \ne 0$, there exists a sequence $\{\mathbf{a}_n\}$ with $\mathbf{a}_n \notin \mathbf{V}(h)$ such that $\lim_{n \to \infty} \mathbf{a}_n = \mathbf{a}$. Because $g(F_i(\mathbf{a}_n)) = g(\mathbf{a}_n)$ and both $g$ and $F_i$ are continuous, we conclude that $g(F_i(\mathbf{a})) = g(\mathbf{a})$ for all $\mathbf{a} \in \mathbf{V}(h)$. Thus, $g(F_i(\mathbf{a})) = g(\mathbf{a})$ for every $\mathbf{a} \in \mathbb{C}^n$, and so $g(F_i(\mathbf{x})) = g(\mathbf{x})$ as polynomials, for all $i \le k$.

($\Leftarrow$) Conversely, assume $g(F_i(\mathbf{x})) = g(\mathbf{x})$ for every $i \le k$. Then for any $i_1, \dots, i_m \in [k]$ and all $\mathbf{a} \in \mathbb{C}^n$, we obtain

$$ g(F_{i_m}(\cdots F_{i_1}(\mathbf{a}))) - g(\mathbf{a}) = 0. $$

Hence $g(\mathbf{x}) - g(\mathbf{a}) \in I_{\mathcal{L}(\mathbf{a}, h, (F_1, \dots, F_k))}$, and $g$ is a universally inductive invariant. $\square$

An invariant is called *inductive* if, once it holds after a single iteration, it continues to hold for all subsequent iterations. By Proposition 7, we immediately obtain:

**Corollary 1** Every universally inductive invariant is inductive.

Algorithm 3 takes as input a sequence $g$ of polynomials in $\mathbb{Q}[\mathbf{x}]$ together with the structure $(\mathbf{f}_1, \dots, \mathbf{f}_k)$ of polynomial maps of a loop, and outputs polynomials defining $\mathcal{U}\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); g)$. The auxiliary procedure $\text{coef}$ takes as input a sequence of polynomials in $\mathbb{Q}[\mathbf{x}, \mathbf{y}]$ and returns the coefficients of the monomials in the variables $\mathbf{x}$. The correctness of Algorithm 3 follows immediately from Proposition 7.
**Algorithm 3 ComputeLoopsUniversal**

**Input:** A sequence **g** = (g₁, ..., gₘ) of polynomials, and polynomials fᵢ,ⱼ,ⱼ ∈ Q[x] for all i ≤ k, j ≤ n, and l ≤ nᵢⱼ.

**Output:** A set of polynomials C₁, ..., Cₜ such that U_C(h, (f₁, ..., fₖ); g) is V(C₁, ..., Cₜ)

1: **for** i ∈ [k] **do**

2: Fᵢ ← (∑<sub>l=1</sub><sup>nᵢ,₁</sup> yᵢ,₁,₁lfᵢ,₁,₁(x), ..., ∑<sub>l=1</sub><sup>nᵢ,ₙ</sup> yᵢ,ₙ,₁lfᵢ,ₙ,₁(x))

3: **end for**

4: {C₁, ..., Cₜ} ← {coef(gᵢ - gᵢ∘Fⱼ) | i ∈ [m], j ∈ [k]}

5: **return** {C₁, ..., Cₜ}

As a concrete application, we demonstrate how our method can be used to synthesize loops that generate Markov triples.

**Example 4 (Markov triples [25])** In this example, we synthesize a loop of the following form that generates a solution to the Markov equation

$$x_1^2 + x_2^2 + x_3^2 - 3x_1x_2x_3 = 0.$$

$$(x_1, x_2, x_3) := (1, 1, 2)$$

while $1 \neq 0$ do

if * then

$$\begin{pmatrix} x_1 \\ x_2 \\ x_3 \end{pmatrix} \leftarrow \begin{array}{l} F_1 \\ \lambda_3 x_1 x_2 + \lambda_4 x_3 + \lambda_5 x_1^2 \\ \lambda_6 x_2 + \lambda_7 x_3 \end{array}$$

else

$$\begin{pmatrix} x_1 \\ x_2 \\ x_3 \end{pmatrix} \leftarrow \begin{array}{l} F_2 \\ \lambda_8 x_1 + \lambda_9 x_2 \\ \lambda_{10} x_2 x_3 + \lambda_{11} x_1 + \lambda_{12} x_2^2 \\ \lambda_{13} x_2 + \lambda_{14} x_3 \end{array}$$

end if

end while

Let $g = x_1^2 + x_2^2 + x_3^2 - 3x_1x_2x_3$. We therefore consider branching loops $\mathcal{L}((1, 1, 2), 1, (F_1, F_2))$ that satisfy the universal polynomial invariant $g$ with structure

$$F_1(\mathbf{x}) = (\lambda_1 x_1 + \lambda_2 x_2, 3x_1 x_2 + \lambda_4 x_3 + \lambda_5 x_1^2, \lambda_6 x_2 + \lambda_7 x_3),$$

$$F_2(\mathbf{x}) = (\lambda_8 x_1 + \lambda_9 x_2, \lambda_{10} x_2 x_3 + \lambda_{11} x_1 + \lambda_{12} x_2^2, \lambda_{13} x_2 + \lambda_{14} x_3)$$

By Proposition 7, we have

$$g(\mathbf{x}) = g(F_1(\mathbf{x})), \quad g(\mathbf{x}) = g(F_2(\mathbf{x})).$$

Hence, the coefficients of the monomials in the variables **x** appearing in the polynomial pairs (g(**x**), g(F₁(**x**))) and (g(**x**), g(F₂(**x**))) must be equal. Hence, we obtain

the following system of 32 polynomial equations:

$$\begin{cases} 3\lambda_1\lambda_3\lambda_6 + 3\lambda_2\lambda_5\lambda_6 - \lambda_3^2 = 0, \\ 3\lambda_8\lambda_{10}\lambda_{13} + 3\lambda_8\lambda_{12}\lambda_{14} = 0 \\ \lambda_5^2 = 0, \\ \dots \\ \lambda_{14}^2 - 1 = 0, \\ \lambda_1^2 - 1 = 0. \end{cases}$$

Using the Z3 solver, we obtain the following solution to the system above:

$$\lambda_2 = \lambda_5 = \lambda_7 = \lambda_8 = \lambda_{12} = \lambda_{13} = 0, \quad \lambda_3 = \lambda_{10} = 3$$

$$\lambda_1 = \lambda_4 = \lambda_6 = \lambda_9 = \lambda_{11} = \lambda_{14} = -1$$

### 3.3.2 Affine case

We now restrict attention to affine universally inductive invariants. We show that U_C(h, (f₁, ..., fₖ); g) is an affine space whenever **g** consists of affine polynomials. Furthermore, we present an algorithm for computing an affine basis of U_C(h, (f₁, ..., fₖ); g).

**Proposition 8** Let **g** = (g₁, ..., gₘ) be affine polynomials. Then the coefficient set U_C(h, (f₁, ..., fₖ); g) is an affine space.

*Proof* Let (b₁, ..., bₖ) ∈ U_C(h, (f₁, ..., fₖ); g). Then, by Proposition 7, the polynomials g₁, ..., gₘ are universally inductive invariants of L(h, (F<sub>f₁,b₁</sub>, ..., F<sub>fₖ,bₖ</sub>)) if and only if

$$g_i(F_j(\mathbf{x})) = g_i(\mathbf{x}) \quad \text{for every } i \le m, j \le k.$$

This condition requires that the coefficients of the monomials in gᵢ(Fⱼ(**x**)) coincide with those in gᵢ(**x**). Since g₁, ..., gₘ are linear, these coefficients are themselves linear polynomials in C[b₁, ..., bₖ]. Consequently, U_C(h, (f₁, ..., fₖ); g) is the solution set of a system of linear equations, and therefore an affine space. □

Proposition 8 shows that, in the affine case, the synthesis problem reduces to a problem of linear algebra.

Let **g** be a sequence of affine polynomials. The following algorithm computes a vector **v** and a basis of a vector space **V** such that U_C(h, (f₁, ..., fₖ); g) is the affine space **v** + **V**.

We now describe the auxiliary procedures used in Algorithm 4:

- **sol** takes as input a sequence of affine polynomials (l₁(**y**), ..., lₜ(**y**)) in Q[y] and returns a solution to the linear system

$$l_1(\mathbf{y}) = 0, \dots, l_r(\mathbf{y}) = 0.$$
- `solveHom` takes as input a sequence of affine polynomials $(l_1(\mathbf{y}), \dots, l_r(\mathbf{y}))$ in $\mathbb{Q}[\mathbf{y}]$ and outputs a basis for the solution space of the corresponding homogeneous system, namely

$$l_1(\mathbf{y}) = 0, \dots, l_r(\mathbf{y}) = 0.$$

The correctness of Algorithm 4 follows immediately from Proposition 8.

**Algorithm 4 ComputeLoopsLinearUniversal**

**Input:** A sequence $\mathbf{g} = (g_1, \dots, g_m)$ of affine polynomials, and polynomials $f_{i,j,l} \in \mathbb{Q}[\mathbf{x}]$ for all $i \le k$, $j \le n$, and $l \le n_{i,j}$.

**Output:** A vector $v \in \mathbb{Q}^M$ and a sequence of vectors $B$ such that $U\mathcal{C}(h, (\mathbf{f}_1, \dots, \mathbf{f}_k); \mathbf{g}) = v + V$, where $V$ is the vector space generated by $B$.

1: $C \leftarrow \text{ComputeLoopsUniversal}(\mathbf{g}, \mathbf{f}_1, \dots, \mathbf{f}_k)$

2: $v \leftarrow \text{sol}(C)$

3: $B \leftarrow \text{solveHom}(C)$

4: **return** $\{v, B\}$

*Example 5* Consider branching loops with a nondeterministic conditional statement involving two branches, defined by

$$F_1(x_1, x_2) = (\lambda_1 x_1^2 + \lambda_2 x_1 + \lambda_3 x_2, \lambda_4 x_1^2 + \lambda_5 x_1 + \lambda_6 x_2),$$

$$F_2(x_1, x_2) = (\lambda_7 x_1 + \lambda_8 x_2, \lambda_9 x_1 + \lambda_{10} x_2),$$

such that $g = x_1 - x_2 + 1$ is a universally inductive invariant of $\mathcal{L}(1, (F_1, F_2))$. By Proposition 7, this requires

$$g(\mathbf{x}) - g(F_1(\mathbf{x})) = 0, \quad g(\mathbf{x}) - g(F_2(\mathbf{x})) = 0.$$

Collecting the coefficients of the monomials in $\mathbf{x}$ yields the linear system:

$$\left\{ \begin{array}{l} \lambda_4 - \lambda_1 = 0, \\ \lambda_5 - \lambda_2 + 1 = 0, \\ \lambda_6 - \lambda_3 - 1 = 0, \\ \lambda_9 - \lambda_7 + 1 = 0, \\ \lambda_{10} - \lambda_8 - 1 = 0. \end{array} \right.$$

A particular solution is $v = (0, 1, -1, 0, 0, 0, 1, -1, 0, 0)$. Solving the associated homogeneous system yields a sequence $B$ of basis vectors:

$$(1, 0, 0, 1, 0, 0, 0, 0, 0), \quad (0, 1, 0, 0, 1, 0, 0, 0, 0),$$

$$(0, 0, 1, 0, 0, 1, 0, 0, 0), \quad (0, 0, 0, 0, 0, 0, 1, 0, 1),$$

$$(0, 0, 0, 0, 0, 0, 0, 1, 0).$$

Therefore, $g$ is a universally inductive invariant of the loop $\mathcal{L}(1, (F_1, F_2))$ if and only if $(\lambda_1, \dots, \lambda_{10}) \in v + \text{span}(B)$.

## 4 Solving Polynomial Systems

In the previous section, we saw that Algorithms 2 and 3 produce systems of multivariate polynomials whose solutions correspond precisely to loops with the prescribed structure and invariants. Thus, the problem of loop synthesis reduces to solving polynomial systems.

Since our goal is to obtain loops that can be represented finitely and exactly on a computer, we focus on rational solutions, i.e., solutions with coefficients in $\mathbb{Q}$. Unlike the situation over $\mathbb{C}$ (where Hilbert's Nullstellensatz applies [26], see also [3, Chap. 4, §1]) or over $\mathbb{R}$ (where the Tarski–Seidenberg theorem applies [27,28], see e.g. [29]), deciding whether a polynomial equation has a rational solution is a long-standing open problem in number theory [30]. For integer solutions, this corresponds to Hilbert's Tenth Problem, which is known to be undecidable [30].

Given these difficulties, we outline three main strategies for addressing the problem, although none is fully satisfactory or complete.

### 4.1 Exploiting the structure of polynomial systems

Although no general algorithm is known for computing (or even deciding the existence of) rational solutions to multivariate polynomial systems by exact methods, many practical instances can still be solved by leveraging structural properties. For example, consider the polynomial system obtained at the end of Example 2. While this case may seem simple or narrowly tailored, all benchmarks reported in Section 5 can be handled in a similar way. More generally, decompositions of varieties with additional structure can sometimes be reduced to combinatorial problems; see, e.g., [31,32].

*Example 6* The variety $V(P_1, \dots, P_4)$ can be decomposed into finitely many irreducible components, which in turn split the system into simpler subsystems. This decomposition can be carried out using classical methods from computer algebra [3, Chap. 4, §6]; here we use the command `minimalPrimes` from Macaulay2 [33]. We obtain the following five irreducible components:

$$V_1 = V(y_5, y_3 + y_4, y_1 + y_2)$$

$$V_2 = V(y_5 + 1, y_3 + y_4 - 1, y_1 + y_2 - 1)$$

$$V_3 = V(y_5 + 1, y_3 + y_4 + 1, y_1 + y_2 - 1)$$

$$V_4 = V(y_3 + y_4 - 1, y_1 + y_2 - 1, y_5^2 - y_5 + 1)$$

$$V_5 = V(y_3 + y_4 + 1, y_1 + y_2 - 1, y_5^2 - y_5 + 1)$$

Thus, $\mathcal{L}((1, 1, -1), 1, F)$ satisfies the polynomial invariants $\{g_1, g_2\}$ if and only if $(\lambda_1, \dots, \lambda_5)$ lies in one of the above components. The simple structure of the defining polynomials makes the problem fully solvable.
For the first three components, which involve only linear polynomials, the problem reduces to standard linear algebra, where efficient methods are available (see e.g., [34]). More specifically, for parameters $\mu_1, \mu_2 \in \mathbb{Q}$, we obtain the following loop maps:

$$V_1: F_1(\mathbf{x}) = (\mu_1(x_1^3 - x_2^2), \mu_2(x_1 - x_2^2), 0)$$

$$V_2: F_2(\mathbf{x}) = (\mu_1 x_1^3 + (1 - \mu_1) x_2^2, \mu_2 x_1 + (1 - \mu_2) x_2^2, -1)$$

$$V_3: F_3(\mathbf{x}) = (\mu_1 x_1^3 - (1 + \mu_1) x_2^2, \mu_2 x_1 + (1 - \mu_2) x_2^2, -1)$$

For the last two components, no rational solution exists, since the polynomial $y_5^2 - y_5 + 1$ has no rational roots.

Another important case arises when the polynomial system computed by Algorithm 2 and Algorithm 3 (or one of its subsystems) has only finitely many solutions. Geometrically, this means that the associated variety (or one of its irreducible components) consists of finitely many points, i.e., it has dimension zero. In this situation, such systems can be reduced (see, e.g., [35, §3], [36]) to polynomial systems with rational coefficients of the form

$$Q_1(x_1) = 0, \quad x_i = Q_i(x_1) \quad \text{for all } i \ge 2.$$

Finding all rational solutions then reduces to solving a univariate polynomial equation, which can be done algorithmically: either through efficient factoring [37, Theorem 15.21] to extract the linear factors in $\mathbb{Q}[x_1]$, or via modular arithmetic-based methods [38].

Thus, whenever the system has finitely many solutions, all rational ones can be effectively computed. Practical implementations exist, such as AlgebraicSolving.jl<fnref n="1" />, which is based on the `msolve` library [39]. Moreover, many benchmarks in the next section fall into this category, which we believe is common when the degree and support of $F$ are comparable.

## 4.2 Numerical methods

Numerical approaches to solving polynomial systems, such as HomotopyContinuation.jl [40], provide powerful tools for approximating solutions. These methods rely on numerical algebraic geometry, in particular on homotopy continuation. Unlike symbolic techniques based on Gröbner bases or resultants, numerical methods can efficiently handle large and complex systems. When applied to the systems generated by Algorithm 2 and Algorithm 3, they yield numerical solutions that can then be checked against nearby integers or rationals to identify valid exact solutions.

**Example 7** Consider the polynomial system $\{P_1, P_2, P_3, P_4\}$ from Example 2. Since it involves five variables and only four equations, it has either no solutions or infinitely many. A common strategy is to augment the system with a random linear form with integer coefficients. Using HomotopyContinuation.jl, we obtain 15 numerical real solutions to the augmented system, 12 of which correspond to valid integer solutions.

Despite their efficiency, numerical methods have limitations. They provide approximate solutions that may lack exact algebraic structure and require additional validation. They can also struggle with singular solutions, and homotopy continuation methods may occasionally miss solutions altogether.

## 4.3 Satisfiability Modulo Theories (SMT) solvers

The SMT solvers decide the satisfiability of logical formulas that combine Boolean logic with background theories such as integer or real arithmetic. In particular, the existence of integer or rational solutions to a polynomial system can be expressed as

$$\exists x_1 \dots \exists x_n (f_1(x_1, \dots, x_n) = 0) \land \dots \land (f_m(x_1, \dots, x_n) = 0).$$

SMT solvers benefit from automated reasoning, efficient decision procedures, and the ability to integrate multiple logical theories. However, they face difficulties with high-degree polynomials and, due to undecidability, cannot guarantee general solutions over the integers. Nevertheless, as shown in Section 5, the SMT solver Z3 successfully finds integer solutions for most of the polynomial systems generated by Algorithms 2 and Algorithm 3.

# 5 Implementation and Experiments

## 5.1 Setup

We implemented Algorithm 2, Algorithm 3 and Algorithm 4 in Macaulay2 [33]. The prototype builds on [22], and the source code is publicly available at:

https://github.com/Erdenebayar2/Synthesizing_Loops.git

All experiments were conducted on a laptop equipped with a 4.8 GHz Intel i7 processor, 16 GB RAM, and a 25 MB L3 cache. After generating polynomial systems using Algorithms 2 and 3, we used the SMT solver Z3 [41] to search for common nonzero integer solutions.

We evaluated our approach on benchmarks from [7, 8, 9]. The benchmark suite is publicly available at:

<footnote n="1">¹ https://algebraic-solving.github.io</footnote>

<footnote>https://github.com/Erdenebayar2/Synthesizing_Loops/software/loops</footnote>
**Notations.** In the following tables, “n” denotes the number of program variables, “m” the number of polynomial invariants in **g**, and “d” their maximal degree. “D” is the maximal degree among the polynomials in **f**₁, ..., **f**ₙ. Let **f**₁ = (f₁, ..., f₁,l₁), ..., **f**ₙ = (fₙ, ..., fₙ,lₙ) be sequences of polynomials in **C[x]**, and set l = l₁ + ... + lₙ. In other words, “l” denotes the total number of generators for the update maps of the loops.

## 5.2 Experimental Results

Table 1 reports the execution times for Algorithm 2 and for Z3, both of which are run on the polynomial systems generated by Algorithm 2. All timings are given in seconds, with a timeout (indicated by **TL**) of 300 seconds. The label “F” indicates that Z3 failed to find an integer solution, while “NI” means that no input was passed to Z3 because Algorithm 2 itself timed out.

In most cases, once Algorithm 2 terminates, Z3 finds a common nonzero integer solution within 0.3 seconds. Thus, searching for integer solutions is not a bottleneck. We also observe that providing additional polynomial invariants generally accelerates the termination of Algorithm 2. Overall, these results demonstrate that the main computational challenge lies in generating the polynomial systems, rather than in solving them with Z3.

<table><caption>**Table 1** Timings for Algorithm 2 in seconds;</caption><thead><tr><th colspan="3">Polynomial map</th><th colspan="2">D=1, l=3</th><th colspan="2">D=1, l=4</th><th colspan="2">D=1, l=5</th><th colspan="2">D=2, l=2</th><th colspan="2">D=2, l=3</th></tr><tr><th>Benchmark</th><th>n</th><th>m</th><th>d</th><th>Alg. 2</th><th>Z3</th><th>Alg. 2</th><th>Z3</th><th>Alg. 2</th><th>Z3</th><th>Alg. 2</th><th>Z3</th><th>Alg. 2</th><th>Z3</th></tr></thead><tbody><tr><td>Ex1.2 [7]</td><td>2</td><td>1</td><td>4</td><td>0.02</td><td>F</td><td>31.1</td><td>F</td><td>TL</td><td>NI</td><td>0.01</td><td>0.06</td><td>TL</td><td>NI</td></tr><tr><td>Ex1.1 [7]</td><td>3</td><td>2</td><td>3</td><td>0.01</td><td>0.06</td><td>0.04</td><td>0.06</td><td>4.4</td><td>0.2</td><td>0.01</td><td>0.06</td><td>0.018</td><td>0.07</td></tr><tr><td>Ex1.1ineq</td><td>3</td><td>2</td><td>3</td><td>0.009</td><td>0.06</td><td>11.4</td><td>0.06</td><td>TL</td><td>NI</td><td>0.008</td><td>0.05</td><td>0.03</td><td>0.05</td></tr><tr><td>Ex5.2[8]</td><td>2</td><td>1</td><td>2</td><td>0.03</td><td>0.17</td><td>0.16</td><td>TL</td><td>TL</td><td>NI</td><td>0.01</td><td>0.07</td><td>0.13</td><td>0.07</td></tr><tr><td>sum1 [9]</td><td>3</td><td>2</td><td>2</td><td>0.02</td><td>0.06</td><td>0.13</td><td>0.06</td><td>1.1</td><td>0.06</td><td>0.01</td><td>0.05</td><td>0.02</td><td>0.06</td></tr><tr><td>square [9]</td><td>2</td><td>1</td><td>2</td><td>0.01</td><td>0.06</td><td>0.5</td><td>TL</td><td>TL</td><td>NI</td><td>0.01</td><td>0.06</td><td>0.015</td><td>0.26</td></tr><tr><td>square.conj [9]</td><td>3</td><td>2</td><td>2</td><td>0.019</td><td>0.06</td><td>0.14</td><td>0.09</td><td>0.39</td><td>0.06</td><td>0.007</td><td>0.05</td><td>0.015</td><td>0.06</td></tr><tr><td>fm11 [9]</td><td>2</td><td>1</td><td>2</td><td>1.19</td><td>0.06</td><td>161.74</td><td>0.06</td><td>TL</td><td>NI</td><td>237.1</td><td>0.06</td><td>TL</td><td>NI</td></tr><tr><td>fm12 [9]</td><td>3</td><td>2</td><td>2</td><td>0.01</td><td>0.06</td><td>0.015</td><td>0.06</td><td>0.017</td><td>0.07</td><td>0.009</td><td>0.07</td><td>0.01</td><td>0.07</td></tr><tr><td>fm13 [9]</td><td>3</td><td>2</td><td>2</td><td>0.01</td><td>0.06</td><td>0.03</td><td>0.05</td><td>0.39</td><td>0.09</td><td>0.01</td><td>0.06</td><td>0.2</td><td>0.11</td></tr><tr><td>intcbrt [9]</td><td>3</td><td>2</td><td>2</td><td>0.25</td><td>0.07</td><td>16.6</td><td>0.08</td><td>TL</td><td>NI</td><td>0.01</td><td>0.06</td><td>0.65</td><td>0.17</td></tr><tr><td>cube.square [9]</td><td>3</td><td>1</td><td>3</td><td>0.01</td><td>0.07</td><td>0.018</td><td>TL</td><td>TL</td><td>NI</td><td>0.15</td><td>0.06</td><td>0.96</td><td>106</td></tr><tr><td>Ex3</td><td>2</td><td>2</td><td>2</td><td>0.014</td><td>0.09</td><td>0.02</td><td>0.1</td><td>0.034</td><td>0.1</td><td>0.13</td><td>0.1</td><td>0.07</td><td>0.12</td></tr><tr><td>markov.triples</td><td>3</td><td>1</td><td>2</td><td>5.61</td><td>0.1</td><td>36.2</td><td>0.1</td><td>134.1</td><td>0.6</td><td>1.35</td><td>0.1</td><td>TL</td><td>NI</td></tr></tbody></table>

Table 2 presents the polynomial systems produced by Algorithm 2, which define $\mathcal{C}(a, h, f; g)$. Similarly, Table 3 shows the systems produced by Algorithm 3, which define $\mathcal{U}\mathcal{C}(h, f; g)$, together with the execution times for Z3 on those systems. For each choice of “D” and “|”, we report the number “s” of nonzero polynomials and whether the system has finitely many solutions. In Tables 2 and 3, “Id” indicates that, within the given structure, the only loop satisfying the specified invariants is the identity map.

Macaulay2 [33] computes the irreducible decomposition of the generated varieties within a few seconds

in most of the cases shown in Tables 2 and 3. In many examples, the irreducible components are defined by linear equations. Furthermore, Table 2 shows that even when the dimension is 0, the varieties are never empty; they always consist of finitely many points.

<table><caption>**Table 2** Data on outputs of Algorithm 2</caption><thead><tr><th colspan="3">Polynomial map</th><th colspan="2">D=1, l=3</th><th colspan="2">D=1, l=4</th><th colspan="2">D=1, l=5</th><th colspan="2">D=2, l=2</th><th colspan="2">D=2, l=3</th></tr><tr><th>Benchmark</th><th>n</th><th>m</th><th>d</th><th>s</th><th>#sols</th><th>s</th><th>#sols</th><th>s</th><th>#sols</th><th>s</th><th>#sols</th><th>s</th><th>#sols</th></tr></thead><tbody><tr><td>Ex1.2 [7]</td><td>2</td><td>1</td><td>4</td><td>3</td><td>&infin;</td><td>4</td><td>&infin;</td><td>TL</td><td>TL</td><td>2</td><td>&infin;</td><td>TL</td><td>TL</td></tr><tr><td>Ex1.1 [7]</td><td>3</td><td>2</td><td>3</td><td>2</td><td>&infin;</td><td>4</td><td>&infin;</td><td>6</td><td>&infin;</td><td>4</td><td>&lt;&infin;</td><td>4</td><td>&lt;&infin;</td></tr><tr><td>Ex1.1ineq</td><td>3</td><td>2</td><td>3</td><td>2</td><td>&infin;</td><td>4</td><td>&infin;</td><td>TL</td><td>TL</td><td>4</td><td>&lt;&infin;</td><td>4</td><td>&lt;&infin;</td></tr><tr><td>Ex5.2[8]</td><td>2</td><td>1</td><td>2</td><td>3</td><td>&infin;</td><td>3</td><td>&infin;</td><td>TL</td><td>TL</td><td>3</td><td>&lt;&infin;</td><td>3</td><td>&infin;</td></tr><tr><td>sum1 [9]</td><td>3</td><td>2</td><td>2</td><td>4</td><td>Id</td><td>6</td><td>&infin;</td><td>6</td><td>&infin;</td><td>2</td><td>&lt;&infin;</td><td>4</td><td>&lt;&infin;</td></tr><tr><td>square [9]</td><td>2</td><td>1</td><td>2</td><td>2</td><td>&infin;</td><td>4</td><td>&infin;</td><td>TL</td><td>TL</td><td>2</td><td>&lt;&infin;</td><td>3</td><td>&infin;</td></tr><tr><td>square.conj [9]</td><td>3</td><td>2</td><td>2</td><td>4</td><td>&lt;&infin;</td><td>6</td><td>&infin;</td><td>6</td><td>&infin;</td><td>4</td><td>&lt;&infin;</td><td>4</td><td>&lt;&infin;</td></tr><tr><td>fm11 [9]</td><td>2</td><td>1</td><td>2</td><td>0</td><td>&infin;</td><td>0</td><td>&infin;</td><td>TL</td><td>TL</td><td>0</td><td>&infin;</td><td>TL</td><td>TL</td></tr><tr><td>fm12 [9]</td><td>3</td><td>2</td><td>2</td><td>2</td><td>&infin;</td><td>4</td><td>&infin;</td><td>TL</td><td>TL</td><td>2</td><td>&lt;&infin;</td><td>4</td><td>&lt;&infin;</td></tr><tr><td>fm13 [9]</td><td>3</td><td>2</td><td>2</td><td>4</td><td>Id</td><td>4</td><td>&infin;</td><td>6</td><td>&infin;</td><td>2</td><td>&lt;&infin;</td><td>4</td><td>&lt;&infin;</td></tr><tr><td>intcbrt [9]</td><td>3</td><td>2</td><td>2</td><td>4</td><td>Id</td><td>4</td><td>&infin;</td><td>TL</td><td>TL</td><td>2</td><td>&lt;&infin;</td><td>4</td><td>&lt;&infin;</td></tr><tr><td>cube.square [9]</td><td>3</td><td>1</td><td>3</td><td>2</td><td>&infin;</td><td>3</td><td>&infin;</td><td>TL</td><td>TL</td><td>3</td><td>&lt;&infin;</td><td>5</td><td>&lt;&infin;</td></tr><tr><td>Ex3</td><td>2</td><td>1</td><td>2</td><td>3</td><td>&infin;</td><td>3</td><td>&infin;</td><td>7</td><td>&infin;</td><td>3</td><td>&lt;&infin;</td><td>7</td><td>&lt;&infin;</td></tr><tr><td>markov.triples</td><td>3</td><td>1</td><td>2</td><td>15</td><td>&lt;&infin;</td><td>15</td><td>&lt;&infin;</td><td>15</td><td>&lt;&infin;</td><td>7</td><td>&lt;&infin;</td><td>TL</td><td>NI</td></tr></tbody></table>

For every benchmark in Table 1, Algorithm 3 terminates within 0.1 seconds and Z3 within 0.3 seconds. However, in most cases the polynomial equations produced by Algorithm 3 either admit no common solution or yield only the identity loop within the specified structure. This limitation arises from the fact that Algorithm 3 assumes the invariants to be universally inductive, whereas Algorithm 2 makes no such assumption.

Accordingly, and because efficiency allows for it, in Table 3 we use significantly larger templates for the update maps of loops than in Table 1. In particular, the number of generators in Table 3 ranges from 6 to 121, compared to only 3 to 5 in Table 1. For these larger templates, Algorithm 2 fails to terminate within 300 seconds mainly because of costly Gröbner basis computations. In contrast, Algorithm 3 always terminates within 0.6 seconds because it relies solely on linear algebra computations. However, it generally produces a loop of a higher degree, which is more susceptible to numerical instability.

In each column of Table 3, the update maps are generated from all monomials up to degree $D$.

<table><caption>**Table 3** Data on outputs of Algorithm 3</caption><thead><tr><th colspan="3">Polynomial map</th><th colspan="2">D=1</th><th colspan="2">D=2</th><th colspan="2">D=3</th></tr><tr><th>Benchmark</th><th>n</th><th>m</th><th>d</th><th>l</th><th>Z3</th><th>s</th><th>#sols</th><th>l</th><th>Z3</th><th>s</th><th>#sols</th></tr></thead><tbody><tr><td>Ex1.2 [7]</td><td>2</td><td>1</td><td>4</td><td>6</td><td>TL</td><td>15</td><td>&lt;&infin;</td><td>12</td><td>TL</td><td>45</td><td>&lt;&infin;</td></tr><tr><td>Ex1.1 [7]</td><td>3</td><td>2</td><td>3</td><td>12</td><td>0.1</td><td>30</td><td>Id</td><td>30</td><td>0.1</td><td>119</td><td>&infin;</td><td>60</td><td>0.15</td><td>304</td><td>TL</td></tr><tr><td>Ex1.1ineq</td><td>3</td><td>2</td><td>3</td><td>12</td><td>0.1</td><td>30</td><td>Id</td><td>30</td><td>0.1</td><td>119</td><td>&infin;</td><td>60</td><td>0.15</td><td>304</td><td>TL</td></tr><tr><td>Ex5.2[8]</td><td>2</td><td>1</td><td>2</td><td>6</td><td>0.1</td><td>6</td><td>&infin;</td><td>12</td><td>0.14</td><td>15</td><td>&infin;</td><td>20</td><td>TL</td><td>28</td><td>&infin;</td></tr><tr><td>sum1 [9]</td><td>3</td><td>2</td><td>2</td><td>12</td><td>0.15</td><td>14</td><td>&infin;</td><td>30</td><td>0.16</td><td>45</td><td>&infin;</td><td>60</td><td>0.17</td><td>104</td><td>TL</td></tr><tr><td>square [9]</td><td>2</td><td>1</td><td>2</td><td>6</td><td>0.1</td><td>6</td><td>&infin;</td><td>12</td><td>0.1</td><td>15</td><td>&infin;</td><td>20</td><td>0.1</td><td>28</td><td>&infin;</td></tr><tr><td>square.conj [9]</td><td>3</td><td>2</td><td>2</td><td>12</td><td>0.1</td><td>14</td><td>&infin;</td><td>30</td><td>0.16</td><td>45</td><td>&infin;</td><td>60</td><td>TL</td><td>104</td><td>TL</td></tr><tr><td>fm11 [9]</td><td>2</td><td>1</td><td>2</td><td>6</td><td>0.14</td><td>6</td><td>&infin;</td><td>12</td><td>0.14</td><td>15</td><td>&infin;</td><td>20</td><td>0.15</td><td>28</td><td>&infin;</td></tr><tr><td>fm12 [9]</td><td>3</td><td>2</td><td>2</td><td>12</td><td>0.15</td><td>14</td><td>&infin;</td><td>30</td><td>0.15</td><td>45</td><td>&infin;</td><td>60</td><td>0.17</td><td>104</td><td>TL</td></tr><tr><td>fm13 [9]</td><td>3</td><td>2</td><td>2</td><td>12</td><td>0.2</td><td>14</td><td>&infin;</td><td>30</td><td>0.15</td><td>45</td><td>&infin;</td><td>60</td><td>0.17</td><td>104</td><td>TL</td></tr><tr><td>intcbrt [9]</td><td>3</td><td>2</td><td>2</td><td>12</td><td>0.17</td><td>30</td><td>Id</td><td>30</td><td>0.2</td><td>119</td><td>&infin;</td><td>60</td><td>0.25</td><td>304</td><td>TL</td></tr><tr><td>cube.square [9]</td><td>3</td><td>1</td><td>3</td><td>12</td><td>0.2</td><td>20</td><td>&infin;</td><td>30</td><td>0.19</td><td>84</td><td>TL</td><td>60</td><td>0.5</td><td>220</td><td>TL</td></tr><tr><td>Ex3</td><td>2</td><td>1</td><td>2</td><td>12</td><td>0.21</td><td>12</td><td>&infin;</td><td>24</td><td>0.2</td><td>30</td><td>&infin;</td><td>40</td><td>0.21</td><td>56</td><td>&infin;</td></tr><tr><td>markov.triples</td><td>3</td><td>1</td><td>2</td><td>24</td><td>TL</td><td>40</td><td>&lt;&infin;</td><td>60</td><td>TL</td><td>168</td><td>&infin;</td><td>121</td><td>TL</td><td>304</td><td>TL</td></tr></tbody></table>
References

1. Floyd, R. Assigning meanings to programs. *Program Verification: Fundamental Issues In Computer Science*. pp. 65-81 (1993)

2. Manna, Z. & Pnueli, A. Temporal verification of reactive systems: safety. (Springer Science & Business Media, 2012)

3. Cox, D., Little, J. & O'Shea, D. Ideals, varieties, and algorithms: an introduction to computational algebraic geometry and commutative algebra. (Springer Science & Business Media, 2013)

4. Kempf, G. Algebraic Varieties. (Cambridge University Press, 1993)

5. Shafarevich, I. & Reid, M. Basic algebraic geometry. (Springer, 1994)

6. Rodríguez-Carbonell, E. & Kapur, D. Automatic generation of polynomial loop invariants: Algebraic foundations. *Proceedings Of The 2004 International Symposium On Symbolic And Algebraic Computation*. pp. 266-273 (2004)

7. Kenison, G., Kovács, L. & Varonka, A. From Polynomial Invariants to Linear Loops. *Proceedings Of The 2023 International Symposium On Symbolic And Algebraic Computation*. pp. 398-406 (2023).

8. Hitarth, S., Kenison, G., Kovács, L. & Varonka, A. Linear Loop Synthesis for Quadratic Invariants. *41st International Symposium On Theoretical Aspects Of Computer Science (STACS 2024)*. 289 pp. 41:1-41:18 (2024)

9. Humenberger, A., Amrollahi, D., Bjørner, N. & Kovács, L. Algebra-Based Reasoning for Loop Synthesis. *Form. Asp. Comput.* 34 (2022,7).

10. Bayarmagnai, E., Mohammadi, F. & Prébet, R. Algebraic Tools for Computing Polynomial Loop Invariants (Extended Version). *ArXiv Preprint arXiv:2412.14043*. (2024)

11. Hrushovski, E., Ouaknine, J., Pouly, A. & Worrell, J. Polynomial invariants for affine programs. *Proceedings Of The 33rd Annual ACM/IEEE Symposium On Logic In Computer Science*. pp. 530-539 (2018)

12. Karr, M. Affine relationships among variables of a program. *Acta Informatica*. 6 pp. 133-151 (1976)

13. Kovács, L. Reasoning algebraically about p-solvable loops. *International Conference On Tools And Algorithms For The Construction And Analysis Of Systems*. pp. 249-264 (2008)

14. Kovács, L. Algebra-Based Loop Analysis. *Proceedings Of The 2023 International Symposium On Symbolic And Algebraic Computation*. pp. 41-42 (2023)

15. Rodríguez-Carbonell, E. & Kapur, D. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. *Science Of Computer Programming*. 64, 54-75 (2007)

16. Rodríguez-Carbonell, E. & Kapur, D. Generating all polynomial invariants in simple loops. *Journal Of Symbolic Computation*. 42, 443-476 (2007)

17. Oliveira, S., Bensalem, S. & Prevosto, V. Synthesizing invariants by solving solvable loops. *International Symposium On Automated Technology For Verification And Analysis*. pp. 327-343 (2017)

18. Hrushovski, E., Ouaknine, J., Pouly, A. & Worrell, J. On strongest algebraic program invariants. *Journal of the ACM*. 70, 1-22 (2023)

19. Ait El Manssour R, Kenison G, Shirmohammadi M, Varonka A. Simple Linear Loops: Algebraic Invariants and Applications. *Proceedings of the ACM on Programming Languages*. 2025 Jan 7;9(POPL):745-71.

20. Srivastava, S., Gulwani, S. & Foster, J. From program verification to program synthesis. *SIGPLAN Not.* 45, 313-326 (2010,1).

21. Goharshady, A., Hitarth, S., Mohammadi, F. & Motwani, H. Algebro-geometric Algorithms for Template-based Synthesis of Polynomial Programs. *Proceedings Of The ACM On Programming Languages*. 7, 727-756 (2023)

22. Bayarmagnai, E., Mohammadi, F. & Prébet, R. Algebraic Tools for Computing Polynomial Loop Invariants. *Proceedings Of The 2024 International Symposium On Symbolic And Algebraic Computation*. pp. 371-381 (2024).

23. Bayarmagnai, E., Mohammadi, F. & Prébet, R. Beyond Affine Loops: A Geometric Approach to Program Synthesis. *Proceedings Of The 14th ACM SIGPLAN International Workshop On The State Of The Art In Program Analysis*. pp. 1-7 (2025)

24. Mayr, E. & Meyer, A. The complexity of the word problem for commutative semi-groups and polynomial ideals. *Advances In Mathematics*. 46 pp. 305-329 (1982)

25. Cassels JW. An introduction to Diophantine approximation, 1957.

26. Hilbert, D. Ueber die vollen Invariantensysteme. *Mathe-matische Annalen*. 42, 313-373 (1893).

27. Tarski, A. & McKinsey, J. A Decision Method for Elementary Algebra and Geometry. (University of California Press, 1951).

28. Seidenberg, A. A New Decision Method for Elementary Algebra. *Annals Of Mathematics*. 60, 365-374 (1954).

29. Basu, S., Pollack, R. & Roy, M. Algorithms in Real Algebraic Geometry. (Springer International Publishing, 2006)

30. Shlapentokh, A. Defining Integers. *The Bulletin Of Symbolic Logic*. 17, 230-251 (2011)

31. Liwski E, Mohammadi F. Solvable and nilpotent matrices: Realizability and irreducible decomposition of their associated varieties. *Journal of Symbolic Computation*, 2025, p. 102484.

32. Liwski E, Mohammadi F, Prébet R. Efficient algorithms for minimal matroid extensions and irreducible decompositions of circuit varieties. *arXiv preprint arXiv:2504.16632*, 2025.

33. Grayson, D. & Stillman, M. Macaulay2, a software system for research in algebraic geometry. (2002)

34. Cook, W. & Steffy, D. Solving Very Sparse Rational Systems of Equations. *ACM Trans. Math. Softw.* 37 (2011,2).

35. Durvye, C. & Lecerf, G. A concise proof of the Kronecker polynomial system solver from scratch. *Expositiones Mathematicae*. 26, 101-139 (2008).

36. Rouillier, F. Solving Zero-Dimensional Systems Through the Rational Univariate Representation. *Applicable Algebra In Engineering, Communication And Computing*. 9, 433-461 (1999)

37. Von Zur Gathen, J. & Gerhard, J. Modern computer algebra. (Cambridge university press, 2013)

38. Loos, R. Computing Rational Zeros of Integral Polynomials by p-Aric Expansion. *SIAM Journal On Computing*. 12, 286-293 (1983)

39. Berthomieu, J., Eder, C. & Safey El Din, M. msolve: A Library for Solving Polynomial Systems. *2021 International Symposium On Symbolic And Algebraic Computation*. pp. 51-58 (2021,7)

40. Breiding, P. & Timme, S. HomotopyContinuation.jl: A Package for Homotopy Continuation in Julia. *Mathematical Software - ICMS 2018*. pp. 458-465 (2018)

41. De Moura, L. & Bjørner, N. Z3: an efficient SMT solver. *Proceedings Of The Theory And Practice Of Software, 14th International Conference On Tools And Algorithms For The Construction And Analysis Of Systems*. pp. 337-340 (2008)