From Polynomial Invariants to Linear Loops

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.

On Inequality Decision Problems for Low-Order Holonomic Sequences

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.