# Beyond Affine Loops: A Geometric Approach to Program Synthesis

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

► To cite this version:

Erdenebayar Bayarmagnai, Fatemeh Mohammadi, Rémi Prébet. Beyond Affine Loops: A Geometric Approach to Program Synthesis. SOAP '25: 14th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, PLDI: Programming Language Design and Implementation, Jun 2025, Seoul, South Korea. pp.1-7, 10.1145/3735544.3735581. hal-05127957

HAL Id: hal-05127957

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

Submitted on 24 Jun 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>
# Beyond Affine Loops: A Geometric Approach to Program Synthesis*

Erdenebayar Bayarmagnai

Fatemeh Mohammadi

Rémi Prébet

erdenebayar.bayarmagnai@kuleuven.be

fatemeh.mohammadi@kuleuven.be

remi.prebet@inria.fr

KU Leuven

KU Leuven

Inria

Belgium

Belgium

France

## 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 polynomial invariants is a crucial task for loops, but it is an undecidable problem 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.

In this paper, we use algebraic geometry tools to design and implement an algorithm that computes a finite set of polynomial equations whose solutions correspond to all loops satisfying the given polynomial invariants. In other words, we reduce the problem of synthesizing loops to finding solutions of polynomial systems within a specified subset of the complex numbers. The latter is handled in our software using an SMT solver.

**CCS Concepts:** • Applied computing → Invariants; Logic and verification; • Computing methodologies → Symbolic and algebraic manipulation.

**Keywords:** Program synthesis, Polynomial invariants

## ACM Reference Format:

Erdenebayar Bayarmagnai, Fatemeh Mohammadi, and Rémi Prébet. 2025. Beyond Affine Loops: A Geometric Approach to Program Synthesis. In *Proceedings of the 14th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP '25), June 16, 2025, Seoul, Republic of Korea*. ACM, New York, NY, USA, 7 pages. https://doi.org/10.1145/3735544.3735581

## 1 Introduction

Loop invariants are properties that hold before and after each iteration and are essential for automating program verification, which ensures correctness before execution. Established methods such as the Floyd-Hoare inductive assertion technique [11] and termination verification via ranking functions [26] rely on loop invariants. A polynomial invariant is a loop invariant expressed as a polynomial equation or inequality.

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

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

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

while $h(x) \neq 0$ do

$$\begin{pmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end{pmatrix} \underset{F}{\leftarrow} \begin{pmatrix} F_1 \\ F_2 \\ \vdots \\ F_n \end{pmatrix}$$

end while

where $x_i$ are the program variables with initial values $a_i$, $h \in \mathbb{C}[x]$, and $F = (F_1, \dots, F_n)$ is a sequence of polynomials in $\mathbb{C}[x]$. The inequality $h(x) \neq 0$, called the *guard*, is assumed to be a single inequality for simplicity (we can replace $h_1 \neq 0, \dots, h_k \neq 0$ with their product $h_1 \dots h_k \neq 0$ without loss of generality). Where there is no $h$ we simply write $\mathcal{L}(a, 1, F)$, which corresponds to an infinite loop.

Previous work [16, 19, 22] has focused on update maps that are restricted to be linear. In this paper, we go beyond this limitation by allowing update maps to be arbitrary polynomial functions. We present a method for computing a system of equations whose common solutions characterize all coefficient assignments for update maps of loops that satisfy a given set of polynomial invariants. To illustrate our main objective, we now present a motivating example.

<footnote>*We are grateful to Teresa Krick for her very helpful comments. The third author is also affiliated with Inria, CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP (UMR 5668), 69342 Lyon Cedex 07, France. The research is partially supported by the KU Leuven grant iBOF/23/064, the FWO grants G0F5921N and G023721N and the ANR grants ANR-20-CE48-0014 NuSCAP and ANR-24-CE48-4035 CNACS</footnote>

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. *SOAP '25, Seoul, Republic of Korea*</footnote>

<footnote>© 2025 Copyright held by the owner/author(s). Publication rights licensed to ACM.</footnote>

<footnote>ACM ISBN 979-8-4007-1922-6/25/06</footnote>

<footnote>https://doi.org/10.1145/3735544.3735581</footnote>
**Example 1.** Consider the following polynomial loop:

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

By applying Algorithm 2, we construct polynomials $P_1, \dots, P_4$, such that $(\lambda_1, \dots, \lambda_5)$ is a common root of these polynomials if and only if the loop satisfies the polynomial invariants $g_1 = x_2^2 - x_1$ and $g_2 = x_3^3 + 2x_2^2 - x_1$. For instance, $(-3, 3, 1, -1, 0)$ is a common root of $\{P_1, \dots, P_4\}$. Thus, if the update map is $F(x_1, x_2, x_3) = (-3x_1^3 + 3x_2^2, x_1 - x_2^2, 0)$, the loop satisfies the invariants $g_1$ and $g_2$. See Example 3 for further details.

**Related works.** The computation of polynomial invariants for loops has been a prominent area of research over the past two decades [3, 9, 17, 20, 23, 24, 27–29]. However, computing invariant ideals is undecidable for general loops [18]. As a result, efficient methods have been developed for restricted classes of loops, particularly those where the assertions are linear or can be transformed into linear assertions.

The converse problem of synthesizing loops from given invariants has received less attention, primarily focusing on linear and affine loops. These studies vary in the types of invariants considered: linear invariants in [34], a single quadratic polynomial in [16], and pure difference binomials in [22]. In contrast, [19] explores general polynomial invariants but lacks the completeness properties of earlier work and does not address guard conditions.

Higher degree loops have been studied in a more general framework in [12, 13], which also takes polynomial inequalities as input. However, the loops synthesized by this algorithm are restricted to those where the input invariants are inductive, meaning that if the invariant holds after one iteration, it holds for all subsequent iterations.

**Our contributions.** We consider the problem of generating polynomial loops with guards from arbitrary polynomial invariants. As a first step, we construct a polynomial system whose solutions correspond precisely to loops with a given structure that satisfy the specified invariants. We then discuss strategies for solving this system. In practice, in most cases a satisfying solution is found using an SMT solver.

Section 2 recalls the definition of invariant sets and key results from [2]. Section 3 introduces a method for identifying multiple polynomial invariants (Proposition 3.5) and proves that the set $\mathscr{C}(a, h, f; g)$ of coefficients of polynomial maps of loops satisfying the invariants $g$ forms an algebraic variety. We also present Algorithm 2, which computes the polynomials defining $\mathscr{C}(a, h, f; g)$. Section 4 discusses strategies for solving polynomial systems and their limitations, while Section 5 presents our algorithm’s implementation and experimental results.

## 2 Preliminaries

In the following, we present some terminology from algebraic geometry. For further details, we refer the reader to [7, 21, 32]. We denote the field of complex numbers by $\mathbb{C}$. Throughout the paper, $\mathbf{x}$ denotes 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 [7, Theorem 4, Chap. 2], every ideal is finitely generated. For a subset $X \subset \mathbb{C}^n$, the defining ideal $I(X)$ consists of all polynomials vanishing on $X$. The radical 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.

Here, we introduce the main object of this paper and build upon key results from [2] by recalling and extending them.

**Definition 2.1.** Let $F : \mathbb{C}^n \to \mathbb{C}^n$ be a map and $X$ be a subset of $\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\}, \\ \text{where } F^{(0)}(x) = x \text{ and } F^{(m)}(x) = F(F^{(m-1)}(x)) \text{ for } m > 1. $$

The following proposition enables the computation of invariant sets using tools from algebraic geometry, relying on the Hilbert Basis Theorem, which implies that descending chains of algebraic varieties eventually stabilize.

**Proposition 2.2.** 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)}$.

Algorithm 1 computes invariant sets via an iterative outer approximation that converges in finitely many steps, based on Proposition 2.2. It relies on the following procedures:

* “Compose” takes as input two sequences of polynomials $g = (g_1, \dots, g_m)$ and $F = (F_1, \dots, F_n)$ in $\mathbb{Q}[\mathbf{x}]$ and outputs the polynomials

$$ g_1(F_1(\mathbf{x}), \dots, F_n(\mathbf{x})), \dots, g_m(F_1(\mathbf{x}), \dots, F_n(\mathbf{x})). $$
* “InRadical” takes as input a sequence of polynomials $\tilde{g}$ and a finite set $S$ in $\mathbb{Q}[\mathbf{x}]$ and outputs “True” if $\tilde{g} \subset \sqrt{\langle S \rangle}$; “False” otherwise.

These procedures are classic routines in symbolic computations, and can be performed using various efficient techniques such as Gröbner bases [7]. See [3] for more details.

**Algorithm 1 InvariantSet**

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

**Output:** Polynomials whose common zero-set is $S_{(F,V(g))}$.

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

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

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

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

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

6: **end while**

7: **return** $S$;

The proof of the termination and correctness of Algorithm 1 follows from Proposition 2.2 and [2, Theorem 2.4].

**Example 2.** Let us compute the invariant set of a polynomial map $F(x_1, x_2) = (2x_1 - 3x_2, x_1 + x_2)$ and an algebraic variety $X = V(x_1^2 - x_2^2 + x_1x_2)$. On input $F$ and $g = x_1^2 - x_2^2 + x_1x_2$, Algorithm 1 computes the invariant set of $F$ and $X$ through the following steps.

* At Step 1, $S$ gets $\{g\}$ and at Step 2, $\tilde{g}$ gets
  $\text{Compose}(g, F) = 5x_1^2 - 15x_2x_2 + 5x_2^2$.

* At Step 3, a Gröbner basis of the ideal $\langle g, 1 - \tilde{g} \rangle$ is computed to verify that

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

* At Step 4, $S$ gets $\{g, g \circ F\}$ and at Step 5, $\tilde{g}$ is set to
  $\text{Compose}(\tilde{g}, F) = -5x_1^2 - 35x_1x_2 + 95x_2^2$.

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

Therefore, the invariant set $S_{(F,V(g))}$ is the vanishing locus of polynomials $\{g, g \circ F\}$.

### 3 From Loops to Polynomial Systems

In this section, we present a method for identifying all loops that satisfy given polynomial invariants by formulating them as solutions of a polynomial system via invariant sets. This reduces the problem to solving a polynomial system, which we explore in the next section.

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

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

or there exists $m \in \mathbb{Z}_{\ge 0}$ such that $g(F^{(m)}(a)) = h(F^{(m)}(a)) = 0$ and for every $l < m$:

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

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

The invariant ideal is an ideal of the ring $\mathbb{C}[x_1, \dots, x_n]$ where $x_1, \dots, x_n$ are program variables [27]. Let $f_1, \dots, f_n$ be polynomials in $\mathbb{C}[x_1, \dots, x_n]$. We denote by $\text{span}\{f_1, \dots, f_n\}$ the vector space they generate.

**Definition 3.3.** $(F_1, \dots, F_n)$ and for $1 \le i \le n$ let $f_i = (f_{i,1}, \dots, f_{i,l_i})$ 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 the map

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

with $F_{\mathbf{f},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 3.4.** Using the notations of Definition 3.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 $a \in \mathbb{C}^n$. Then, the polynomial loop, structured by $\mathbf{f}$, with invariants including $g$, is defined by the coefficient set:

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

In simple words, $\mathcal{C}(a, h, \mathbf{f}; g)$ is the set of all 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(x) \neq 0 do
x \leftarrow F_{\mathbf{f},b}(x)
end while
```

We now give a necessary and sufficient condition for checking whether given polynomials are loop invariants. This extends [3, Proposition 2.7], where the following statement was proven for a single polynomial invariant.

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

$$ 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 $a \in \mathbb{C}^n$, $g \subset I_{\mathcal{L}(a,h,F)}$ if and only if $(a, 1) \in S_{(G_h, X)}$.

**Proof.** Let $X_i = V(zg_i) \subset \mathbb{C}^{n+1}$ be an algebraic variety for $i \in \{1, \dots, m\}$. For any $i \in \{1, \dots, m\}$, by [3, Proposition 2.7], $g_i \in I_{\mathcal{L}(a,h,F)}$ if and only if $(a, 1) \in S_{(G_h, X_i)}$. Therefore, $g_1, \dots, g_m \in I_{\mathcal{L}(a,h,F)}$ if and only if

$$ (a, 1) \in S_{(G_h, X_1)} \cap \dots \cap S_{(G_h, X_m)}. $$
It follows directly from Definition 2.1 that

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

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

In the following proposition, we present a necessary and sufficient condition for loops with a given structure to satisfy specified polynomial invariants.

**Proposition 3.6.** For $1 \le i \le n$, let $\mathbf{f}_i = (f_{i,1}, \dots, f_{i,l_i})$ be sequences of polynomials in $\mathbb{C}[\mathbf{x}]$ and define $\mathbf{f} = (\mathbf{f}_1, \dots, \mathbf{f}_n)$. Let $z, y_{1,1}, \dots, y_{1,l_1}, y_{n,1}, \dots, y_{n,l_n}$ be new indeterminates, let $h \in \mathbb{C}[\mathbf{x}]$ and define the following polynomial map in $\mathbb{C}[\mathbf{x}, y, z]$:

$$G_{y,h}(\mathbf{x}, y, z) = \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}), y, zh(\mathbf{x}) \right).$$

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

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

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

$$\mathcal{C}(\mathbf{a}, \mathbf{h}, \mathbf{f}; \mathbf{g}) = \{\mathbf{b} \in \mathbb{C}^{l_1+\dots+l_n} \mid (\mathbf{a}, \mathbf{b}, 1) \in S_{(G_{y,h},X)}\}.$$

*Proof.* Write $G_{y,h}(\mathbf{x}, y, z) = (G_y(\mathbf{x}, y), zh(\mathbf{x}))$ where

$$G_y(\mathbf{x}, 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}), y \right).$$

By Proposition 3.5, $g_1, \dots, g_m$ are polynomial invariants of $\mathcal{L}((\mathbf{a}, \mathbf{b}), h, G_y)$ if and only if $(\mathbf{a}, \mathbf{b}, 1) \in S_{(G_{y,h},X)}$. Since the value of $y$ remains $\mathbf{b}$ after any iteration, we know that

$$F_y^N(\mathbf{x}, \mathbf{b}) = (F^N(\mathbf{x}), \mathbf{b})$$

for any $N \in \mathbb{N}$. Therefore, $\mathbf{g} \subset I_{\mathcal{L}(\mathbf{a},h,F_{\mathbf{b}})}$ if and only if $\mathbf{g} \subset I_{\mathcal{L}((\mathbf{a},\mathbf{b}),h,G_y)}$, that is $(\mathbf{a}, \mathbf{b}, 1) \in S_{(G_{y,h},X)}$ by above. $\square$

Since the invariant set is an algebraic variety, by Proposition 3.6, $\mathcal{C}(\mathbf{a}, \mathbf{h}, \mathbf{f}; \mathbf{g})$ is also an algebraic variety. Specifically, its defining equations are obtained by substituting $\mathbf{x} = \mathbf{a}$ and $z = 1$ into the system defining the invariant set.

We now present our main algorithm for computing the polynomials that define $\mathcal{C}(\mathbf{a}, \mathbf{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}, \mathbf{h}, \mathbf{f}; \mathbf{g})$ is $\mathcal{V}(P_1, \dots, P_s)$

$$1: G_{y,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}), y, zh(\mathbf{x}) \right);$$

$$2: \{Q_1, \dots, Q_s\} \leftarrow \text{InvariantSet}((zg_1, \dots, zg_m), G_{y,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: \text{return } \{P_1, \dots, P_s\};$$

We now prove the correctness of Algorithm 2.

**Theorem 3.7.** Let $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}]$. Let $\mathbf{a} \in \mathbb{Q}^n$ and define $\mathbf{f} = (\mathbf{f}_1, \dots, \mathbf{f}_n)$. On input $\mathbf{a}, \mathbf{h}, \mathbf{f}, \mathbf{g}$, Algorithm 2 outputs a set of polynomials such that the vanishing locus of the polynomials is $\mathcal{C}(\mathbf{a}, \mathbf{h}, \mathbf{f}; \mathbf{g})$.

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

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

such that $S_{(G_{y,h},X)}$ is the common solution of $\{Q_1, \dots, Q_s\}$. Therefore, by Proposition 3.6, $g_1, \dots, g_m$ are polynomial invariants of $\mathcal{L}(\mathbf{a}, \mathbf{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{b}})}$ if and only if

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

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

**Example 3.** Consider the loop $\mathcal{L}((1, 1, -1), 1, F)$ together with polynomial invariants $g_1$ and $g_2$ from Example 1. Let us compute all loops with the polynomial map $F$ that satisfy the polynomial invariants $g_1$ and $g_2$. That is, we determine all loops of the given form with the precondition $(x_1 = 1, x_2 = 1, x_3 = -1)$ and the postcondition $(x_2^2 - x_1 = 0, x_3^3 + 2x_2^2 - x_1 = 0)$. Let $F = (F_1, F_2, F_3)$, $\mathbf{g} = \{g_1, g_2\}$ and define

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

From the structure of a loop, we know that

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

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

$$G_{y,h}(\mathbf{x}, 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, y, z)$$

At Step 2, on input $G_{y,h}$ and $X$, algorithm “InvariantSet” computes polynomials whose vanishing locus is the invariant set $S_{(G_{y,h},X)}$ and outputs $\{Q_1(\mathbf{x}, y, z), \dots, Q_6(\mathbf{x}, y, z)\}$. After substituting the initial values of the loop into the polynomials, we obtain only four non-zero polynomials $P_1(\mathbf{y}), P_2(\mathbf{y}), P_3(\mathbf{y})$ and $P_4(\mathbf{y})$ whose common vanishing locus is $\mathcal{C}((1, 1, -1), 1, \mathbf{f}; \mathbf{g})$:

$$P_1 = (y_3 + y_4)^2 - y_1 - y_2; \quad 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_2^3 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_1^3 y_2 - 3y_1^2 y_2^2 - y_1 y_2^3 + 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_4^4 y_4^2 + 4y_3^3 y_4^3 + 6y_3^2 y_4^4 + 4y_3 y_4^5 + y_6^4 + 2y_1 y_3 y_4 + 2y_2 y_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_1^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.$$
# 4 Polynomial System Solving

In the previous section, we have seen how Algorithm 2 can compute a system of multivariate polynomials whose solutions correspond exactly to the loops with the given structures and invariants. This approach reduces the problem of loop synthesis to solving polynomial systems.

However, since we aim to find loops with finite, exact representations on computers, we focus on rational solutions. Unlike solutions in $\mathbb{C}$ (by Hilbert's Nullstellensatz [15], see e.g., [7, Chap. 4, §1]) or $\mathbb{R}$ (via Tarski-Seidenberg's theorem [31, 35], see e.g., [1]), determining whether a multivariate polynomial equation has a rational solution is a major open problem in number theory [33]. For integer solutions, this is Hilbert's Tenth Problem, which is undecidable [33]. We outline three main strategies to address this, though none is fully satisfactory or complete.

## 4.1 Exploit Structure

Although no general algorithm is known to compute (or even decide the existence of) rational solutions to multivariate polynomials using exact methods, many real-world cases can still be successfully addressed with existing techniques. To illustrate this, consider the polynomial system obtained at the end of Example 3. While this example may appear overly simplistic or too specific, it turns out that all benchmarks presented in Section 5 can be tackled in a similar manner.

**Example 4.** The variety $V(P_1, \dots, P_4)$ can be decomposed into finitely many irreducible components, which in turn decompose the system into potentially simpler subsystems. This can be done using classical methods from computer algebra [7, Chap. 4, §6], and here we apply the “minimalPrimes” command from Macaulay2 [14]. We obtain the following five components:

$$ 
\begin{aligned}
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)
\end{aligned}
$$

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 irreducible components. The well-structured polynomials defining each component allow us to fully solve the problem.

For the first three components, which involve only linear polynomials, the problem reduces to a standard linear algebra routine, benefiting from optimized methods (see e.g., [6]). More specifically, if $\mu_1$ and $\mu_2$ are parameters in $\mathbb{Q}$, we obtain the following loop map:

$$ 
\begin{aligned}
V_1: F_1(x_1, x_2, x_3) &= (\mu_1(x_1^3 - x_2^2), \mu_2(x_1 - x_2^2), 0) \\
V_2: F_2(x_1, x_2, x_3) &= (\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(x_1, x_2, x_3) &= (\mu_1 x_1^3 - (1 + \mu_1)x_2^2, \mu_2 x_1 + (1 - \mu_2)x_2^2, -1)
\end{aligned}
$$

For the last two components, there is no rational solution, because the last equation $y_5^2 - y_5 + 1$ has no rational roots.

Another specific case occurs when the polynomial system computed by Algorithm 2 (or a subsystem of it) has only finitely many solutions. Geometrically, this means the associated variety (or an irreducible component) consists of finitely many points, i.e., has dimension zero. In this case, such systems can be reduced (see e.g., [10, §3] and [30]) to polynomial systems with rational coefficients of the form:

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

This reduces to finding all rational solutions of a univariate polynomial, which is either done using arithmetic-based modular algorithms [25] or efficient factoring algorithms to identify its linear factors in $\mathbb{Q}[x_1]$ [36, Theorem 15.21].

Thus, when the system has finitely many solutions, we can always find all rational ones. Efficient software, such as AlgebraicSolving.jl<fnref n="1" />, based on the msolve library [4], is designed for such tasks. Many of the benchmarks in the next section involve polynomial systems of this type, which we expect when the degree and support of $F$ are close.

## 4.2 Numerical Methods

Numerical methods for solving polynomial systems, such as HomotopyContinuation.jl [5], provide powerful tools for approximating solutions. These methods use numerical algebraic geometry, particularly homotopy continuation. Unlike symbolic approaches that rely on Gröbner bases or resultants, numerical methods can efficiently handle large and complex systems. Using these methods, we can find numerical solutions of the polynomial system generated by Algorithm 2 and check if close integers or rational numbers are valid solutions of the polynomial system.

**Example 5.** Consider the polynomial system $\{P_1, \dots, P_4\}$ from Example 3. This system either has no solutions or infinitely many, as there are 5 variables and only 4 equations. A classic approach to handle this is to introduce a random linear form with integer coefficients. Using HomotopyContinuation.jl, we find 15 numerical real solutions to the augmented system, 12 of which correspond to valid integer solutions.

Despite their efficiency, numerical methods have several drawbacks. First, they provide approximate solutions, which may lack exact algebraic structure and require further validation. Second, these methods can struggle with singular solutions. Additionally, homotopy continuation techniques may occasionally miss solutions.

## 4.3 Satisfiability Modulo Theories (SMT) Solvers

SMT solvers determine the satisfiability of logical formulas combining Boolean logic with mathematical theories, such as integer or real arithmetic. By verifying the satisfiability of $\exists x_1 \dots \exists x_n (f_1(x_1, \dots, x_n) = 0) \wedge \dots \wedge (f_m(x_1, \dots, x_n) = 0)$, one can determine the existence of integer or rational solutions to a system of polynomial equations.

<footnote n="1">¹https://algebraic-solving.github.io</footnote>
SMT solvers leverage automated reasoning, efficient decision procedures, and integration with other logical theories. However, they can struggle with high-degree polynomials and may fail to find general integer solutions due to undecidability. Nevertheless, as discussed in Section 5, the SMT solver Z3 we used successfully finds integer solutions for most systems of polynomials generated by Algorithm 2.

# 5 Implementation and Experiments

In this section, we present the implementation of Algorithm 2 and report experiments on benchmarks from related works [16, 19, 22], which are limited to generating linear loops. The implementation in Macaulay2 [14] is available at

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

After running Algorithm 2, we use the SMT solver Z3 [8] to find a common nonzero integer solution for the polynomials.

## 5.1 Implementation Details

The experiments below were performed on a laptop equipped with a 4.8 GHz Intel i7 processor, 16 GB of RAM and 25 MB L3 cache. This prototype implementation is primarily based on the one in [2] to which we refer for further details.

## 5.2 Experimental Results

Let $f_1 = (f_{1,1}, \dots, f_{1,l_1}), \dots, f_n = (f_{n,1}, \dots, f_{n,l_n})$ and $g = (g_1, \dots, g_m)$ be sequences of polynomials in $\mathbb{C}[\mathbf{x}]$, and define $\mathbf{f} = (f_1, \dots, f_n)$. Let $h \in \mathbb{C}[\mathbf{x}]$. In Tables 1 and 2, we present the outputs and timings for Algorithm 2, which computes polynomials whose vanishing locus is $\mathscr{C}(\mathbf{a}, \mathbf{h}, \mathbf{f}; g)$, along with timings for Z3 [8] for finding a common non-zero integer solution to the polynomials generated by Algorithm 2. The first row shows the benchmarks, while the first column describes the structures of the polynomial maps of loops. The benchmarks sources are available at

https://github.com/Erdenebayar2/Synthesizing_Loops/software/loops

Table 1 presents the execution timings for Algorithm 2 and Z3 [8], both using polynomial equations generated by Algorithm 2. Timings are in seconds, with a timeout of 300 seconds. “F” indicates Z3 failed to find an integer solution, while “NI” denotes no input was provided to Z3 when the algorithm reached the time limit.

In the following tables, $n$ denotes the number of program variables, $m$ is the number of polynomial invariants $g$ and $d$ is the maximal degree of polynomial invariants $g$. Moreover, $D$ denotes the maximal degrees of polynomials in $f_1, \dots, f_n$, and $l = l_1 + \dots + l_n$.

In most cases, when Algorithm 2 terminates, Z3 quickly finds a common non-zero integer solution for the generated polynomials within 0.3 seconds. Thus, finding a non-zero integer solution is not a bottleneck in our approach. The primary computational bottleneck lies in generating the polynomial systems for loop generation. Additionally, we

observe that as more polynomial invariants are provided, Algorithm 2 terminates faster.

<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></tr></thead><tbody><tr><td>Ex2</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></tr><tr><td>Ex3</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>Ex3Ineq</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>Ex4</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</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</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</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>fmi1</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>fmi2</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>fmi3</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</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</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></tbody></table>

Table 2 presents the output of Algorithm 2, which is a polynomial system whose solution set exactly corresponds to $\mathscr{C}(\mathbf{a}, \mathbf{h}, \mathbf{f}; g)$. For each choice of $D$ and $l$, we report the number $s$ of non-zero polynomials in the output system and indicate whether or not there are finitely many solutions.

<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>Ex2</td><td>2</td><td>1</td><td>4</td><td>3</td><td>∞</td><td>4</td><td>∞</td><td>TL</td><td>TL</td><td>2</td><td>∞</td><td>TL</td><td>TL</td></tr><tr><td>Ex3</td><td>3</td><td>2</td><td>3</td><td>2</td><td>∞</td><td>4</td><td>∞</td><td>6</td><td>∞</td><td>4</td><td>&lt;∞</td><td>4</td><td>&lt;∞</td></tr><tr><td>Ex3Ineq</td><td>3</td><td>2</td><td>3</td><td>2</td><td>∞</td><td>4</td><td>∞</td><td>TL</td><td>TL</td><td>4</td><td>&lt;∞</td><td>4</td><td>&lt;∞</td></tr><tr><td>Ex4</td><td>2</td><td>1</td><td>2</td><td>3</td><td>∞</td><td>3</td><td>∞</td><td>TL</td><td>TL</td><td>3</td><td>&lt;∞</td><td>3</td><td>∞</td></tr><tr><td>sum1</td><td>3</td><td>2</td><td>2</td><td>4</td><td>∞</td><td>6</td><td>∞</td><td>6</td><td>∞</td><td>2</td><td>&lt;∞</td><td>4</td><td>&lt;∞</td></tr><tr><td>square</td><td>2</td><td>1</td><td>2</td><td>2</td><td>∞</td><td>4</td><td>∞</td><td>TL</td><td>TL</td><td>2</td><td>∞</td><td>3</td><td>∞</td></tr><tr><td>square_conj</td><td>3</td><td>2</td><td>2</td><td>4</td><td>&lt;∞</td><td>6</td><td>∞</td><td>6</td><td>∞</td><td>4</td><td>&lt;∞</td><td>4</td><td>&lt;∞</td></tr><tr><td>fmi1</td><td>2</td><td>1</td><td>2</td><td>0</td><td>∞</td><td>0</td><td>∞</td><td>TL</td><td>TL</td><td>0</td><td>∞</td><td>TL</td><td>TL</td></tr><tr><td>fmi2</td><td>3</td><td>2</td><td>2</td><td>2</td><td>∞</td><td>4</td><td>∞</td><td>4</td><td>∞</td><td>2</td><td>&lt;∞</td><td>4</td><td>&lt;∞</td></tr><tr><td>fmi3</td><td>3</td><td>2</td><td>2</td><td>4</td><td>&lt;∞</td><td>4</td><td>∞</td><td>6</td><td>∞</td><td>2</td><td>&lt;∞</td><td>4</td><td>&lt;∞</td></tr><tr><td>intcbrt</td><td>3</td><td>2</td><td>2</td><td>4</td><td>&lt;∞</td><td>4</td><td>∞</td><td>TL</td><td>TL</td><td>2</td><td>&lt;∞</td><td>4</td><td>&lt;∞</td></tr><tr><td>cube square</td><td>3</td><td>1</td><td>3</td><td>2</td><td>∞</td><td>3</td><td>∞</td><td>TL</td><td>TL</td><td>3</td><td>&lt;∞</td><td>5</td><td>&lt;∞</td></tr></tbody></table>

We observe that Macaulay2 [14] computed the irreducible decompositions of varieties defined by the polynomials generated by Algorithm 2 in most cases within a few seconds. In many instances, the irreducible components of the varieties are defined by linear equations. In Table 2, even when the dimension of the varieties is 0, the varieties are not empty in all cases, indicating that they consist of finitely many points.

# 6 Conclusion

We presented a method for generating polynomial loops with specified structures that satisfy given polynomial invariants, reducing the problem to solving a system of polynomial equations. Along with an algorithm for constructing this system, we discussed various strategies for solving it. While previous work has primarily focused on linear maps, our approach extends beyond this limitation, marking a significant advancement in the synthesis of non-linear programs.

This work opens up several promising avenues for future research. A natural next step would be to explore the synthesis of more complex loop structures, such as branching and nested loops. Additionally, extending the approach to handle polynomial invariants in the form of inequalities, rather than just equations, could greatly enhance the flexibility and applicability of the method.
References

[1] Saugata Basu, Richard Pollack, and Marie-Françoise Roy. 2006. Algorithms in Real Algebraic Geometry (2nd revised and extended 2016 ed.). Springer International Publishing. doi:10.1007/3-540-33099-2

[2] Erdenebayar Bayarmagnai, Fatemeh Mohammadi, and Rémi Prébet. 2024. Algebraic Tools for Computing Polynomial Loop Invariants. In Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation (Raleigh, NC, USA) (ISSAC '24). Association for Computing Machinery, New York, NY, USA, 371–381. doi:10.1145/3666000.3669710

[3] Erdenebayar Bayarmagnai, Fatemeh Mohammadi, and Rémi Prébet. 2024. Algebraic Tools for Computing Polynomial Loop Invariants (Extended Version). arXiv preprint arXiv:2412.14043 (2024).

[4] Jérémy Berthomieu, Christian Eder, and Mohab Safey El Din. 2021. msolve: A Library for Solving Polynomial Systems. In 2021 International Symposium on Symbolic and Algebraic Computation. ACM, Saint Petersburg, Russia, 51–58. doi:10.1145/3452143.3465545

[5] Paul Breiding and Sascha Timme. 2018. HomotopyContinuation.jl: A Package for Homotopy Continuation in Julia. In Mathematical Software - ICMS 2018. Springer International Publishing, Cham, 458–465. doi:10.1007/978-3-319-96418-8_54

[6] William Cook and Daniel E. Steffy. 2011. Solving Very Sparse Rational Systems of Equations. ACM Trans. Math. Softw. 37, 4, Article 39 (Feb. 2011), 21 pages. doi:10.1145/1916461.1916463

[7] David Cox, John Little, and Donal O’Shea. 2013. Ideals, varieties, and algorithms: an introduction to computational algebraic geometry and commutative algebra. Springer Science & Business Media. doi:10.1007/978-3-319-16721-3

[8] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340. doi:10.1007/978-3-540-78800-3_24

[9] Steven de Oliveira, Saddek Bensalem, and Virgile Prevosto. 2017. Synthesizing invariants by solving solvable loops. In International Symposium on Automated Technology for Verification and Analysis. Springer, 327–343. doi:10.1007/978-3-319-68167-2_22

[10] Clémence Durvye and Grégoire Lecerf. 2008. A concise proof of the Kronecker polynomial system solver from scratch. Expositiones Mathematicae 26, 2 (2008), 101–139. doi:10.1016/j.exmath.2007.07.001

[11] Robert Floyd. 1993. Assigning meanings to programs. In Program Verification: Fundamental Issues in Computer Science. Springer, 65–81. doi:10.1007/978-94-011-1793-7_4

[12] Amir Goharshady, S. Hitarth, Fatemeh Mohammadi, and Harshit Motwani. 2023. Algebro-geometric Algorithms for Template-based Synthesis of Polynomial Programs (Full Version including Appendices). https://hal.science/hal-04012686. (2023).

[13] Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, and Harshit Jitendra Motwani. 2023. Algebro-geometric Algorithms for Template-based Synthesis of Polynomial Programs. Proceedings of the ACM on Programming Languages 7, OOPSLA1 (2023), 727–756. doi:10.1145/3586052

[14] Daniel R Grayson and Michael E Stillman. 2002. Macaulay2, a software system for research in algebraic geometry.

[15] David Hilbert. 1893. Ueber die vollen Invariantensysteme. Math. Ann. 42, 3 (1893), 313–373. doi:10.1007/BF01444162

[16] S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. 2024. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024), Vol. 289. 41:1–41:18. doi:10.4230/LIPlcs.STACS.2024.41

[17] Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. 2018. Polynomial invariants for affine programs. In Proceedings of

the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. 530–539. doi:10.1145/3209108.3209142

[18] Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. 2023. On strongest algebraic program invariants. J. ACM 70, 5 (2023), 1–22. doi:10.1145/3614319

[19] Andreas Humenberger, Daneshvar Amrollahi, Nikolaj Bjørner, and Laura Kovács. 2022. Algebra-Based Reasoning for Loop Synthesis. Form. Asp. Comput. 34, 1 (2022), 31 pages. doi:10.1145/3527458

[20] Michael Karr. 1976. Affine relationships among variables of a program. Acta Informatica 6 (1976), 133–151. doi:10.1007/BF00268497

[21] G. Kempf. 1993. Algebraic Varieties. Cambridge University Press. doi:10.1017/CBO9781107359956

[22] George Kenison, Laura Kovács, and Anton Varonka. 2023. From Polynomial Invariants to Linear Loops. In Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (Tromsø, Norway) (ISSAC '23). Association for Computing Machinery, New York, NY, USA, 398–406. doi:10.1145/3597066.3597109

[23] Laura Kovács. 2008. Reasoning algebraically about p-solvable loops. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 249–264. doi:10.1007/978-3-540-78800-3_18

[24] Laura Kovács. 2023. Algebra-Based Loop Analysis. In Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation. 41–42. doi:10.1145/3597066.3597150

[25] Rüdiger Loos. 1983. Computing Rational Zeros of Integral Polynomials by p-Adic Expansion. SIAM J. Comput. 12, 2 (1983), 286–293. doi:10.1137/0212017

[26] Zohar Manna and Amir Pnueli. 2012. Temporal verification of reactive systems: safety. Springer Science & Business Media. doi:10.1007/978-1-4612-4222-2

[27] Enric Rodríguez-Carbonell and Deepak Kapur. 2004. Automatic generation of polynomial loop invariants: Algebraic foundations. In Proceedings of the 2004 international symposium on Symbolic and algebraic computation. 266–273. doi:10.1145/1005285.1005324

[28] Enric Rodríguez-Carbonell and Deepak Kapur. 2007. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming 64, 1 (2007), 54–75. doi:10.1016/j.scico.2006.03.003

[29] Enric Rodríguez-Carbonell and Deepak Kapur. 2007. Generating all polynomial invariants in simple loops. Journal of Symbolic Computation 42, 4 (2007), 443–476. doi:10.1016/j.jsc.2007.01.002

[30] Fabrice Rouillier. 1999. Solving Zero-Dimensional Systems Through the Rational Univariate Representation. Applicable Algebra in Engineering, Communication and Computing 9, 5 (1999), 433–461. doi:10.1007/s002000050114

[31] A. Seidenberg. 1954. A New Decision Method for Elementary Algebra. Annals of Mathematics 60, 2 (1954), 365–374. https://doi.org/10.2307/1969640

[32] Igor Rostislavovich Shafarevich and Miles Reid. 1994. Basic algebraic geometry. Vol. 1. Springer. doi:10.1007/978-3-642-37956-7

[33] Alexandra Shlapentokh. 2011. Defining Integers. The Bulletin of Symbolic Logic 17, 2 (2011), 230–251. doi:10.2178/bsl/1305810912

[34] Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From program verification to program synthesis. SIGPLAN Not. 45, 1 (Jan. 2010), 313–326. doi:10.1145/1707801.1706337

[35] Alfred Tarski and J. C. McKinsey. 1951. A Decision Method for Elementary Algebra and Geometry (dgo - digital original, 1 ed.). University of California Press. https://doi.org/10.1525/9780520348097

[36] Joachim Von Zur Gathen and Jürgen Gerhard. 2013. Modern computer algebra. Cambridge university press. doi:10.1017/CBO9781139856065

Received 2025-03-05; accepted 2025-04-25