Synthesizing Invariant Clusters for Polynomial Programs by Semidefinite Programming

TL;DR

This paper introduces a new method using semidefinite programming to efficiently synthesize invariant clusters for polynomial programs, enabling reusable invariants and extending to more general templates.

Contribution

It proposes a novel SDP-based approach for synthesizing invariant clusters, avoiding symbolic routines and achieving near-complete parameter inclusion under standard assumptions.

Findings

SDP hierarchy effectively synthesizes invariant sets

Method avoids symbolic quantifier elimination

Extends to semialgebraic and non-polynomial functions

Abstract

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.