用半定规划生成非线性插值函数
Generating Non-Linear Interpolants by Semidefinite Programming
摘要：
基于插值的技术已经广泛且成功地应用于硬件和软件的验证，例如，在有界模型检验、CEGAR、SMT等中，最难的部分是如何合成插值。为发现命题逻辑的内插、一阶理论的无量词片段及其组合而进行的各种工作已经被提出。然而，很少有工作集中在发现多项式插值在文献中。本文给出了一种基于半定规划的非线性插值的构造方法，并通过实例说明了如何将这些结果应用于程序的验证。
英文摘要：
Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model check- ing, CEGAR, SMT, etc., whose hardest part is how to synthesize interpolants. Various work for discovering interpolants for propositional logic, quantifier-free fragments of first-order theories and their combinations have been proposed. However, little work focuses on discovering polynomial interpolants in the literature. In this paper, we provide an approach for constructing non-linear interpolants based on semidefinite programming, and show how to apply such results to the verification of programs by examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
