二次多项式不等式的插值综合及与EUF的组合
Interpolation synthesis for quadratic polynomial inequalities and combination with EUF
摘要：
提出了一种为严格和非严格二次多项式不等式的合取公式生成插值函数的算法。该算法是基于一个关键的观察，二次多项式不等式可以线性化，如果他们是凹的。利用时间复杂度为$\mathcal{O}(n^3+nm))$的半定规划，证明了Motzkin转置定理的一个推广，该定理用于生成两个相互矛盾的多项式不等式合取之间的插值，其中$n$是变量数，$m$是不等式数.利用\cite{SSLMCS2008}提出的无量词理论组合插值的框架，给出了凹二次多项式不等式与不可解释函数符号上的等式理论的组合算法（\textit{EUF}）.该方法适用于所有现有的抽象域，如\emph{octagon}、\emph{polyhedra}、\emph{ellipsoid}等，因此可以用于提高现有程序和混合系统验证技术的可扩展性.此外，我们还讨论了如何使用Gröbner基将我们的方法扩展到凹二次多项式之外的公式。
英文摘要：
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öbner basis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
