  The template-based method is one of the most successful approaches to
algebraic invariant synthesis. In this method, an algorithm designates a
template polynomial p over program variables, generates constraints for p=0 to
be an invariant, and solves the generated constraints. However, this approach
often suffers from an increasing template size if the degree of a template
polynomial is too high.
  We propose a technique to make template-based methods more efficient. Our
technique is based on the following finding: If an algebraic invariant exists,
then there is a specific algebraic invariant that we call a generalized
homogeneous algebraic invariant that is often smaller. This finding justifies
using only a smaller template that corresponds to a generalized homogeneous
algebraic invariant.
  Concretely, we state our finding above formally based on the abstract
semantics of an imperative program proposed by Cachera et al. Then, we modify
their template-based invariant synthesis so that it generates only generalized
homogeneous algebraic invariants. This modification is proved to be sound.
Furthermore, we also empirically demonstrate the merit of the restriction to
generalized homogeneous algebraic invariants. Our implementation outperforms
that of Cachera et al. for programs that require a higher-degree template.
