Generating Program Invariants via Interpolation
This work addresses the challenge of program verification for developers and researchers, though it is incremental as it builds on existing methods for invariant generation.
The authors tackled the problem of automatically generating polynomial equations as inductive loop invariants for computer programs, proposing a new algorithm based on polynomial interpolation that is efficient and applicable to a broader range of problems, as demonstrated by experiments on a large collection of programs.
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).