# Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences

## TL;DR

This paper introduces a novel method for automatically generating all polynomial invariants for loops with complex arithmetic, including multiplication, by transforming programs into recurrence relations and applying algebraic techniques.

## Contribution

The paper presents a new approach that extends the class of P-solvable loops handled by invariant generation, incorporating multiplication with loop counters and using Gr"obner basis computation.

## Key findings

- Successfully computes polynomial invariants for complex loops
- Extends the class of loops for which invariants can be automatically generated
- Implemented in the Aligator Mathematica package

## Abstract

Analyzing and reasoning about safety properties of software systems becomes an especially challenging task for programs with complex flow and, in particular, with loops or recursion. For such programs one needs additional information, for example in the form of loop invariants, expressing properties to hold at intermediate program points. In this paper we study program loops with non-trivial arithmetic, implementing addition and multiplication among numeric program variables. We present a new approach for automatically generating all polynomial invariants of a class of such programs. Our approach turns programs into linear ordinary recurrence equations and computes closed form solutions of these equations. These closed forms express the most precise inductive property, and hence invariant. We apply Gr\"obner basis computation to obtain a basis of the polynomial invariant ideal, yielding thus a finite representation of all polynomial invariants. Our work significantly extends the class of so-called P-solvable loops by handling multiplication with the loop counter variable. We implemented our method in the Mathematica package Aligator and showcase the practical use of our approach.