Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis

Abstract

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.