• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Generating Non-linear Interpolants by Semidefinite Programming
【24h】

Generating Non-linear Interpolants by Semidefinite Programming

机译：通过半定编程生成非线性插值

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model checking, CEGAR, SMT, etc., in which the 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.
机译：基于插值的技术已广泛且成功地应用于硬件和软件的验证，例如，在边界模型检查，CEGAR，SMT等中，其中最难的部分是如何合成插值。已经提出了各种用于发现命题逻辑的插值器，一阶理论的无量词片段及其组合的工作。但是，很少有工作致力于发现文献中的多项式内插。在本文中，我们提供了一种基于半定规划的构造非线性插值的方法，并通过示例展示了如何将这些结果应用于程序验证。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号