  In this paper, we present a novel approach to synthesize invariant clusters
for polynomial programs. An invariant cluster is a set of program invariants
that share a common structure, which could, for example, be used to save the
needs for repeatedly synthesizing new invariants when the specifications and
programs are evolving. To that end, we search for sets of parameters $R_k$
w.r.t. a parameterized multivariate polynomial $I(a, x)$ (i.e. a template) such
that $I(a, x) \leq 0$ is a valid program invariant for all $a \in R_k$. Instead
of using time-consuming symbolic routines such as quantifier eliminations, we
show that such sets of parameters can be synthesized using a hierarchy of
semidefinite programming (SDP). Moreover, we show that, under some standard
non-degenerate assumptions, almost all possible valid parameters can be
included in the synthesized sets. Such kind of completeness result has
previously only been provided by symbolic approaches. Further extensions such
as using semialgebraic and general algebraic templates (instead of polynomial
ones) and allowing non-polynomial continuous functions in programs are also
discussed.
