• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议> >Efficient Generation of Small Interpolants in CNF
【24h】

Efficient Generation of Small Interpolants in CNF

机译：CNF中小插值的高效生成

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

摘要

Interpolation-based model checking (ITP) is an efficient and complete model checking procedure. However, for large problems, interpolants generated by ITP might become extremely large, rendering the procedure slow or even intractable. In this work we present a novel technique for interpolant generation in the context of model checking. The main novelty of our work is that we generate small interpolants in Conjunctive Normal Form (CNF) using a twofold procedure: First we propose an algorithm that exploits resolution refutation properties to compute an interpolant approximation. Then we introduce an algorithm that takes advantage of inductive reasoning to turn the interpolant approximation into an interpolant. Unlike ITP, our approach maintains only the relevant subset of the resolution refutation. In addition, the second part of the procedure exploits the properties of the model checking problem at hand, in contrast to the general-purpose algorithm used in ITP. We developed a new interpolation-based model checking algorithm, called CNF-ITP. Our algorithm takes advantage of the smaller interpolants and exploits the fact that the interpolants are given in CNF. We integrated our method into a SAT-based model checker and experimented with a representative subset of the HWMCC'12 benchmark set. Our experiments show that, overall, the interpolants generated by our method are 42 times smaller than those generated by ITP. Our CNF-ITP algorithm outperforms ITP, and at times solves problems that ITP cannot solve. We also compared CNF-ITP to the successful IC3 algorithm. We found that CNF-ITP outperforms IC3 in a large number of cases.
机译：基于插值的模型检查（ITP）是高效而完整的模型检查过程。但是，对于较大的问题，ITP生成的插值可能会变得非常大，从而使过程缓慢甚至难以处理。在这项工作中，我们在模型检查的背景下提出了一种用于内插生成的新技术。我们工作的主要新颖之处在于，我们使用双重过程生成了合取范式（CNF）的小内插值：首先，我们提出了一种利用分辨率反驳属性计算内插逼近的算法。然后，我们介绍一种利用归纳推理将插值逼近转换为插值的算法。与ITP不同，我们的方法仅维护分辨率反驳的相关子集。此外，与ITP中使用的通用算法相比，该过程的第二部分利用了手头模型检查问题的性质。我们开发了一种新的基于插值的模型检查算法，称为CNF-ITP。我们的算法利用较小的插值，并利用CNF中给出插值的事实。我们将我们的方法集成到基于SAT的模型检查器中，并使用HWMCC'12基准集的代表性子集进行了实验。我们的实验表明，总体而言，我们的方法生成的内插比ITP生成的内插小42倍。我们的CNF-ITP算法优于ITP，有时可以解决ITP无法解决的问题。我们还将CNF-ITP与成功的IC3算法进行了比较。我们发现CNF-ITP在许多情况下都优于IC3。

著录项

  • 来源
    《》|2013年|330-346|共17页
  • 会议地点 Saint Petersburg(RU)
  • 作者

    Yakir Vizel; Vadim Ryvchin; Alexander Nadel;

  • 作者单位

    Computer Science Department, The Technion, Haifa, Israel;

    Information Systems Engineering Department, The Technion, Haifa, Israel ,Design Technology Solutions Group, Intel Corporation, Haifa, Israel;

    Design Technology Solutions Group, Intel Corporation, Haifa, Israel;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号