Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences

Authors:
  • AHAndreas Humenberger
    Andreas Humenberger
  • MJMaximilian Jaroschek
    Maximilian Jaroschek
  • LKLaura Kovács
    Laura Kovács
Preprint
Publisher website
Google Scholar
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.

This publication has 10 references indexed in Scilit: