Generating Program Invariants via Interpolation

TL;DR

This paper introduces an efficient polynomial interpolation-based algorithm for automatically generating inductive loop invariants in programs, demonstrating its effectiveness through experiments and theoretical analysis of invariant properties.

Contribution

It presents a novel polynomial interpolation algorithm for invariant generation, expanding applicability beyond existing methods and providing theoretical insights into invariant ideal properties.

Findings

Algorithm is efficient and applicable to many problems

Experimental results show effectiveness on diverse programs

Theoretical conditions for existence of invariants are established

Abstract

This article focuses on automatically generating polynomial equations that are inductive loop invariants of computer programs. We propose a new algorithm for this task, which is based on polynomial interpolation. Though the proposed algorithm is not complete, it is efficient and can be applied to a broader range of problems compared to existing methods targeting similar problems. The efficiency of our approach is testified by experiments on a large collection of programs. The current implementation of our method is based on dense interpolation, for which a total degree bound is needed. On the theoretical front, we study the degree and dimension of the invariant ideal of loops which have no branches and where the assignments define a P-solvable recurrence. In addition, we obtain sufficient conditions for non-trivial polynomial equation invariants to exist (resp. not to exist).