Interpolation synthesis for quadratic polynomial inequalities and combination with EUF

TL;DR

This paper introduces an algorithm for generating interpolants for conjunctions of quadratic polynomial inequalities, leveraging concavity to linearize them, and extends the approach to combined theories with EUF, enhancing verification scalability.

Contribution

It proposes a novel interpolation algorithm for quadratic inequalities based on a generalized Motzkin's theorem and combines it with EUF for broader applicability.

Findings

Algorithm operates in polynomial time $ ext{O}(n^3+nm)$

Applicable to various abstract domains like octagon and polyhedra

Extends to formulas beyond concave quadratics using Gröbner basis

Abstract

An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict) is proposed. The algorithm is based on a key observation that quadratic polynomial inequalities can be linearized if they are concave. A generalization of Motzkin's transposition theorem is proved, which is used to generate an interpolant between two mutually contradictory conjunctions of polynomial inequalities, using semi-definite programming in time complexity $\mathcal{O}(n^3+nm))$, where $n$ is the number of variables and $m$ is the number of inequalities. Using the framework proposed by \cite{SSLMCS2008} for combining interpolants for a combination of quantifier-free theories which have their own interpolation algorithms, a combination algorithm is given for the combined theory of concave quadratic polynomial inequalities and the equality theory over uninterpreted functions symbols (\textit{EUF}). The proposed approach is applicable to all existing abstract domains like \emph{octagon}, \emph{polyhedra}, \emph{ellipsoid} and so on, therefore it can be used to improve the scalability of existing verification techniques for programs and hybrid systems. In addition, we also discuss how to extend our approach to formulas beyond concave quadratic polynomials using Gr\"{o}bner basis.