Invariant Generation for Multi-Path Loops with Polynomial Assignments

TL;DR

This paper presents an algorithm for generating all polynomial invariants of extended P-solvable loops with polynomial assignments, using Gr"obner basis computation, and demonstrates its efficiency and termination properties.

Contribution

The paper introduces a novel iterative algorithm employing Gr"obner bases to compute polynomial invariants for multi-path loops with polynomial assignments, proving its termination and efficiency.

Findings

Algorithm computes polynomial invariants for extended P-solvable loops.

Fixed point reached after linearly bounded iterations based on variables and branches.

Implementation in Aligator shows improved efficiency over existing methods.

Abstract

Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properties are typically expressed as loop invariants. In this paper we study a class of multi-path program loops with numeric variables, in particular nested loops with conditionals, where assignments to program variables are polynomial expressions over program variables. We call this class of loops extended P-solvable and introduce an algorithm for generating all polynomial invariants of such loops. By an iterative procedure employing Gr\"obner basis computation, our approach computes the polynomial ideal of the polynomial invariants of each program path and combines these ideals sequentially until a fixed point is reached. This fixed point represents the polynomial ideal of all polynomial invariants of the given extended P-solvable loop. We prove termination of our method and show that the maximal number of iterations for reaching the fixed point depends linearly on the number of program variables and the number of inner loops. In particular, for a loop with m program variables and r conditional branches we prove an upper bound of m*r iterations. We implemented our approach in the Aligator software package. Furthermore, we evaluated it on 18 programs with polynomial arithmetic and compared it to existing methods in invariant generation. The results show the efficiency of our approach.