# Polynomial Invariant Generation for Non-deterministic Recursive Programs

arXiv: https://arxiv.org/abs/1902.04373 · HTML: https://mlsanity.com/paper/1902.04373/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Feb 2019.

## Built on by (most cited first, 3 of 3)

- [Geometry of Radial Basis Neural Networks for Safety Biased Approximation of Unsafe Regions](https://mlsanity.com/paper/2210.05596/) (2022)
- [Quantitative Verification of Omega-regular Properties in Probabilistic Programming](https://mlsanity.com/paper/2512.21596/) (2025)
- [Entropy Objectives in Markov Decision Processes](https://mlsanity.com/paper/2606.21726/) (2026)

## Abstract (arXiv)

We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set. To the best of our knowledge, this is the first invariant generation method to provide completeness guarantees for invariants consisting of polynomial inequalities. Moreover, on the theoretical side, the worst-case complexity of our approach is subexponential, whereas the worst-case complexity of the previously-known complete method (Colon et al, CAV 2003), which could only handle linear invariants, is exponential. On the practical side, we reduce the invariant generation problem to quadratic programming (QCLP), which is a classical optimization problem with many industrial solvers. Finally, we demonstrate the applicability of our approach by providing experimental results on several academic benchmarks.