RealCertify: a Maple package for certifying non-negativity
Victor Magron, Mohab Safey El Din

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 (resp. ) be the field of rational (resp. real) numbers and be variables. Deciding the non-negativity of polynomials in over or over semi-algebraic domains defined by polynomial constraints in 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Polynomial and algebraic computation
