• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Finite Model Finding in SMT
【24h】

Finite Model Finding in SMT

机译：SMT中的有限模型发现

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

摘要

SMT solvers have been used successfully as reasoning engines for automated verification. Current techniques for dealing with quantified formulas in SMT are generally incomplete, forcing SMT solvers to report "unknown" when they fail to prove the unsatisfiability of a formula with quantifiers. This inability to return counter-models limits their usefulness in applications that produce quantified verification conditions. We present a novel finite model finding method that reduces these limitations in the case of quantifiers ranging over free sorts. Our method contrasts with previous approaches for finite model finding in first-order logic by not relying on the introduction of domain constants for the free sorts and by being fully integrated into the general architecture used by most SMT solvers. This integration is achieved through the addition of a novel solver for sort cardinality constraints and a module for quantifier instantiation over finite domains. Initial experiments with verification conditions generated from a deductive verification tool developed at Intel Corp. show that our approach compares quite favorably with the state of the art in SMT.
机译：SMT求解器已成功用作自动验证的推理引擎。当前在SMT中处理量化公式的技术通常是不完善的，当SMT求解器无法证明量词无法满足公式要求时，迫使他们报告“未知”。这种无法返回的反模型限制了它们在产生量化验证条件的应用程序中的有用性。我们提出了一种新颖的有限模型查找方法，该方法可减少在自由排序范围内的量词的情况下的这些限制。我们的方法与以前在一阶逻辑中进行有限模型查找的方法不同，该方法不依赖于为自由排序引入域常数，而是完全集成到大多数SMT求解器使用的通用体系结构中。通过添加用于排序基数约束的新颖求解器和用于有限域上的量词实例化的模块，可以实现这种集成。由英特尔公司开发的演绎验证工具生成的验证条件的初步实验表明，我们的方法与SMT的最新技术相比具有优势。

著录项

  • 来源
    《Computer aided verification》|2013年|640-655|共16页
  • 会议地点 Saint Petersburg(RU)
  • 作者

    Andrew Reynolds; Cesare Tinelli; Amit Goel; Sava Krstic;

  • 作者单位

    Department of Computer Science, The University of Iowa;

    Department of Computer Science, The University of Iowa;

    Strategic CAD Labs, Intel Corporation;

    Strategic CAD Labs, Intel Corporation;

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

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号