Quadratic Zonotopes:An extension of Zonotopes to Quadratic Arithmetics

TL;DR

This paper introduces quadratic zonotopes, extending affine forms to quadratic forms for static analysis, along with a semi-definite programming algorithm for projection, with implementation and practical examples.

Contribution

It proposes quadratic zonotopes as an extension of affine zonotopes and develops a semi-definite programming method for their projection, enhancing static analysis capabilities.

Findings

Quadratic zonotopes effectively model convex sets with quadratic error terms.

The semi-definite programming algorithm accurately projects quadratic zonotopes to intervals.

Implementation demonstrates practical applicability on representative examples.

Abstract

Affine forms are a common way to represent convex sets of $\mathbb{R}$ using a base of error terms $\epsilon \in [-1, 1]^m$. Quadratic forms are an extension of affine forms enabling the use of quadratic error terms $\epsilon_i \epsilon_j$. In static analysis, the zonotope domain, a relational abstract domain based on affine forms has been used in a wide set of settings, e.g. set-based simulation for hybrid systems, or floating point analysis, providing relational abstraction of functions with a cost linear in the number of errors terms. In this paper, we propose a quadratic version of zonotopes. We also present a new algorithm based on semi-definite programming to project a quadratic zonotope, and therefore quadratic forms, to intervals. All presented material has been implemented and applied on representative examples.