  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).
