Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis

Concretely, we state and prove our finding above formally. Then, we modify the template-based algorithm proposed by Cachera et al. so that it generates only generalized homogeneous polynomials. This modification is proved to be sound. Furthermore, we also empirically demonstrate the merit of the restriction to generalized homogeneous polynomials. Our implementation outperforms that of Cachera et al. for programs that require a higher-degree template.