• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Symposium on Asynchronous Circuits and Systems >A Survey of Acceleration Techniques for SMT-Based Bounded Model Checking
【24h】

A Survey of Acceleration Techniques for SMT-Based Bounded Model Checking

机译：基于SMT的有界模型检查的加速技术综述

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Model checking is wildly acknowledged to be an effective formal technique for verifying that a finite state system satisfies desired properties expressed in temporal logic. There are primarily two types of model checking approaches: explicit model checking and symbolic model checking. To mitigate the notorious state exploration problems suffered by explicit model checking, bounded model checking (BMC) has been proposed as an alternative to other symbolic model checking approaches based on binary decision diagrams. Although originally SAT solvers are used by BMC as the reasoning engine, a recent trend is to switch from SAT to SMT solvers. In this paper, we survey contributions on acceleration of SMT-based BMC. In addition, we discuss some related techniques that could be potentially used as well for the acceleration purpose.
机译：人们普遍认为，模型检查是一种有效的形式技术，用于验证有限状态系统是否满足时间逻辑表示的期望属性。主要有两种类型的模型检查方法：显式模型检查和符号模型检查。为了缓解显式模型检查所遭受的臭名昭著的状态探索问题，提出了有界模型检查（BMC）作为基于二进制决策图的其他符号模型检查方法的替代方法。尽管BMC最初将SAT求解器用作推理引擎，但最近的趋势是从SAT转换为SMT求解器。在本文中，我们调查了基于SMT的BMC在加速方面的贡献。此外，我们讨论了一些可能也可用于加速目的的相关技术。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号