Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization

TL;DR

This paper introduces a novel method for generating polynomial invariants using sums-of-squares optimization, enabling property-driven verification of programs with complex polynomial behaviors.

Contribution

It presents a new approach that combines sums-of-squares programming with invariant generation guided by specific properties or state space zones.

Findings

Successfully generates polynomial invariants for programs with polynomial updates.

Applicable to programs with disjunctive polynomial control structures.

Evaluated on various programs demonstrating effectiveness.

Abstract

While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties is not easily compatible with the usual forward fixpoint computation using numerical abstract domains. We propose here to rely on sums-of-squares programming to characterize a property-driven polynomial invariant. This invariant generation can be guided by either boundedness, or in contrary, a given zone of the state space to avoid. While the target property is not necessarily inductive with respect to the program semantics, our method identifies a stronger inductive polynomial invariant using numerical optimization. Our method applies to a wide set of programs: a main while loop composed of a disjunction (if-then-else) of polynomial updates e.g. piecewise polynomial controllers. It has been evaluated on various programs.