TCS Journal 2018 Journal Article
Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis
- Kensuke Kojima
- Minoru Kinoshita
- Kohei Suenaga
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 p = 0 is an algebraic invariant, then p can be decomposed into the sum of specific polynomials that we call generalized homogeneous polynomials, that are often smaller. This finding justifies using only a smaller template that corresponds to generalized homogeneous polynomials. 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.