Publications

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodríguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

It is a longstanding open problem whether there is an algorithm to decide the Positivity Problem for linear recurrence sequences (LRS) over the integers, namely whether given such a sequence, all its terms are non-negative. Decidability is known for LRS of order $5$ or less, i.e., for those sequences in which every new term depends linearly on the previous five (or fewer) terms. For simple LRS (i.e., those sequences whose characteristic polynomials have no repeated roots), decidability of Positivity is known up to order $9$. In this paper, we focus on the important subclass of reversible LRS, i.e., those integer LRS $\langle u_n \rangle_{n=0}^\infty$ whose bi-infinite completion $\langle u_n \rangle_{n=-\infty}^\infty$ also takes exclusively integer values; a typical example is the classical Fibonacci (bi-)sequence $\langle \dots, 5, -3, 2, -1, 1, 0, 1, 1, 2, 3, 5, \ldots \rangle$. Our main results are that Positivity is decidable for reversible LRS of order $11$ or less, and for simple reversible LRS of order $17$ or less.

Hypergeometric sequences are rational-valued sequences that satisfy first-order linear recurrence relations with polynomial coefficients; that is, a hypergeometric sequence $\langle u_n \rangle$ is one that satisfies a recurrence of the form $f(n)u_n = g(n)u_{n-1}$ where $f,g \in \mathbb{Z}[x]$. In this paper, we consider the Membership Problem for hypergeometric sequences: given a hypergeometric sequence $\langle u_n \rangle$ and a target value $t\in \mathbb{Q}$, determine whether $u_n=t$ for some index $n$. We establish decidability of the Membership Problem under the assumption that either (i) $f$ and $g$ have distinct splitting fields or (ii) $f$ and $g$ are monic polynomials that both split over a quadratic extension of $\mathbb{Q}$. Our results are based on an analysis of the prime divisors of polynomial sequences $\langle f(n) \rangle$ and $\langle g(n) \rangle$ appearing in the recurrence relation.

Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive arguments that are key in automating the verification of program loops. The problem of generating loop invariants; in particular, invariants described by polynomial relations (so called polynomial invariants), is therefore one of the hardest problems in software verification. In this paper we advocate an alternative solution to invariant generation. Rather than inferring invariants from loops, we synthesise loops from invariants. As such, we generate loops that satisfy a given set of polynomials; in other words, our synthesised loops are correct by construction. Our work turns the problem of loop synthesis into a symbolic computation challenge. We employ techniques from algebraic geometry to synthesise loops whose polynomial invariants are described by pure difference binomials. We show that such complex polynomial invariants need ``only’’ linear loops, opening up new venues in program optimisation. We prove the existence of non-trivial loops with linear updates for polynomial invariants generated by pure difference binomials. Importantly, we introduce an algorithmic approach that constructs linear loops from such polynomial invariants, by generating linear recurrence sequences that have specified algebraic relations among their terms.

The membership and threshold problems for recurrence sequences are fundamental open decision problems in automated verification. The former problem asks whether a chosen target is an element of a sequence, whilst the latter asks whether every term in a sequence is bounded from below by a given value. A rational-valued sequence $\langle u_n \rangle_n$ is hypergeometric if it satisfies a first-order linear recurrence of the form $p(n)u_{n+1} = q(n)u_{n}$ with polynomial coefficients $p,q\in\mathbb{Z}[x]$. In this note we establish decidability results for the aforementioned problems for restricted classes of hypergeometric sequences. For example, we establish decidability for the aforementioned problems under the assumption that the polynomial coefficients $p,q\in\mathbb{Z}[x]$ are monic and split over an imaginary rational extension of $\mathbb{Q}$. We also establish conditional decidability results; that is, conditional on Schanuel’s conjecture, when the irreducible factors of the monic polynomial coefficients $p,q\in\mathbb{Z}[x]$ are either linear or quadratic.

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodríguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

Given an integer linear recurrence sequence $\langle X_n \rangle$, the Skolem Problem asks to determine whether there is a natural number $n$ such that $X_n=0$. In a recent paper (LICS 2022), Lipton, Luca, Nieuwveld, Ouaknine, Purser, and Worrell prove that the Skolem Problem is decidable for a class of reversible sequences up to order seven. Here we give an alternative proof of the result. The novelty of our approach arises from our use of results concerning the polynomial relations between Galois conjugates. In particular, we make repeated use of a result due to Dubickas and Smyth for algebraic integers that lie alongside all their Galois conjugates on two (but not one) concentric circles centred at the origin.

An infinite sequence $\langle u_n \rangle$ of real numbers is holonomic if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is positive if each $u_n \geq 0$, and minimal if, given any other linearly independent sequence $\langle v_n \rangle$ satisfying the same recurrence relation, the ratio $u_n/v_n$ converges to $0$ as $n$ tends to infinity. In this paper we establish a Turing reduction of the problem of deciding positivity of second-order holonomic sequences to that of deciding minimality of such sequences. More specifically, we give a procedure for determining positivity of second-order holonomic sequences that terminates in all but an exceptional number of cases, and we show that in these exceptional cases positivity can be determined using an oracle for deciding minimality.

An infinite sequence $\langle u_n \rangle$ of real numbers is holonomic if it satisfies a linear recurrence relation with polynomial coefficients: $g_{k+1}(n)u_{n+k} = g_k(n)u_{n+k-1} + \cdots + g_1(n)u_n$ where each coefficient $g_0, \ldots, g_k \in \mathbb{Q}[n]$. Here $k$ is the order of the sequence; order-1 holonomic sequences are also known as hypergeometric sequences. The degree of the sequence is the highest degree of the polynomial coefficients appearing in the recurrence relation. A holonomic sequence $\langle u_n \rangle$ is said to be positive if each $u_n \geq 0$, and minimal if, given any other linearly independent sequence $\langle v_n \rangle$ satisfying the same recurrence relation, the ratio $u_n/v_n$ converges to $0$. Given two hypergeometric sequences $\langle u_n \rangle$ and $\langle v_n \rangle$, the Hypergeometric Inequality Problem asks whether, for all $n$, $u_n \leq v_n$. In this paper, we focus on various decision problems for second-order and hypergeometric sequences, and in particular on effective reductions concerning such problems. Some of these reductions also involve certain numerical quantities (known as periods, exponential periods, and pseudoperiods, originating from algebraic geometry and number theory), and classical decision problems regarding equalities among these quantities. We establish the following:

• For second-order holonomic sequences, the Positivity Problem reduces to the Minimality Problem.
• For second-order, degree-1 holonomic sequences, the Positivity and Minimality Problems both reduce to the Equality Problems for exponential periods and pseudoperiods.
• The Hypergeometric Inequality Problem reduces to the Pseudoperiod Equality Problem.

The Skolem Problem asks, given a linear recurrence sequence $(u_n)$, whether there exists $n\in\mathbb{N}$ such that $u_n = 0$. In this paper we consider the following specialisation of the problem: given in addition $c\in\mathbb{N}$, determine whether there exists $n\in\mathbb{N}$ of the form $n = lp^k$, with $k, l \leq c$ and $p$ any prime number, such that $u_n = 0$.

In this paper, we establish statistical results for a convex co-compact action of a free group on a CAT(−1) space where we restrict to a non-trivial conjugacy class in the group. In particular, we obtain a central limit theorem where the variance is twice the variance that appears when we do not make this restriction.

In this paper we study the action of the fundamental group of a finite metric graph on its universal covering tree. We assume the graph is finite, connected and the degree of each vertex is at least three. Further, we assumean irrationality condition on the edge lengths. We obtain an asymptotic for the number of elements in a fixed conjugacy class for which the associated displacement of a given base vertex in the universal covering tree is at most $T$. Under a mild extra assumption we also obtain a polynomial error term.