RealCertify: a Maple package for certifying non-negativity

TL;DR

RealCertify is a Maple package that certifies polynomial non-negativity over the rationals using sum of squares certificates and semi-definite programming, aiding applications in engineering and verification.

Contribution

It introduces a hybrid symbolic-numeric approach in Maple for certifying polynomial non-negativity over rationals, expanding computational tools in symbolic algebra.

Findings

Successfully certifies non-negativity using sum of squares certificates.

Applicable to engineering, verification, and cyber-physical systems.

Utilizes semi-definite programming for efficient computation.

Abstract

Let $\mathbb{Q}$ (resp. $\mathbb{R}$) be the field of rational (resp. real) numbers and $X = (X_1, \ldots, X_n)$ be variables. Deciding the non-negativity of polynomials in $\mathbb{Q}[X]$ over $\mathbb{R}^n$ or over semi-algebraic domains defined by polynomial constraints in $\mathbb{Q}[X]$ is a classical algorithmic problem for symbolic computation. The Maple package \textsc{RealCertify} tackles this decision problem by computing sum of squares certificates of non-negativity for inputs where such certificates hold over the rational numbers. It can be applied to numerous problems coming from engineering sciences, program verification and cyber-physical systems. It is based on hybrid symbolic-numeric algorithms based on semi-definite programming.