• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Conference on Tools with Artificial Intelligence >On Selecting Constraints for Replication in Model Checking
【24h】

On Selecting Constraints for Replication in Model Checking

机译：在模型检查中选择复制约束

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

摘要

Model Checking is an important formal method for software and hardware verification. Bounded Model Checking (BMC) and k-induction are both parameterized methods, often working together: BMC focus on bug finding, while k-induction searches for an inductive invariant. Both of them greatly rely on their underlying decision procedure, e.g. on their SAT/SMT solver. By construction, BMC and k-induction formulas can be partitioned into 3 sets, one of them being perfectly symmetric (w.r.t. the unrolling mechanism). We propose in this paper to efficiently take advantage of these symmetries in order to perform learnt clauses replications. Replicating learnt clauses was already suggested in the early years of BMC, but unfortunately abandoned because of its tendency to drown the solver with too many clauses. Recently, constraints replication has been extended to temporal induction, a technique that combines BMC and k-induction, using assumption literals to detect replicable clauses. We propose to revisit constraints replications for temporal induction in a number of new ways. First, we highlight that adding assumption literals to transition relations, as it was done recently, have a non-negligible negative impact in practice. Then, we confirm that the replication of too many clauses in the learnt clause database is also prejudicial in most of the cases, even in temporal induction. Hence, we propose to limit the replication to external (outside the solver) replication only. This allows an even simpler strategy to detect replicable clauses, which requires almost no modification of both the SAT solver and the encoding strategy used in the model checker. Then, we show that, by carefully selecting learnt clauses to replicate, we improve our model checker performance, thus challenging the common belief about clauses replications. As a last contribution, we show that ZigZag, an algorithm that combines BMC and k-induction inside a single solver, is more efficient when performed backward.
机译：模型检查是用于软件和硬件验证的重要正式方法。边界模型检查（BMC）和k归纳法都是参数化方法，通常一起使用：BMC专注于错误查找，而k归纳法搜索归纳不变式。他们两个都极大地依赖于他们的基本决策程序，例如在他们的SAT / SMT求解器上。通过构造，BMC和k归纳公式可以分为3组，其中一组是完全对称的（具有展开机制）。我们在本文中建议有效利用这些对称性来执行学习的子句复制。在BMC的早期，已经有人建议复制学习过的子句，但不幸的是，由于它倾向于使求解器淹没过多的子句，因此被放弃了。最近，约束复制已扩展到时间归纳法，这是一种结合BMC和k归纳法的技术，它使用假设文字来检测可复制的子句。我们建议以多种新方式重新审视用于时间归纳的约束条件复制。首先，我们强调指出，将假设文字添加到过渡关系中（如最近所做的那样）在实践中具有不可忽略的负面影响。然后，我们确认，在大多数情况下，即使是在时间归纳中，在学习的子句数据库中复制过多的子句也是有偏见的。因此，我们建议将复制限制为仅外部（在求解程序外部）复制。这允许使用甚至更简单的策略来检测可复制子句，这几乎不需要修改SAT求解器和模型检查器中使用的编码策略。然后，我们表明，通过仔细选择要复制的学习子句，可以提高模型检查器的性能，从而挑战了关于子句复制的普遍信念。作为最后的贡献，我们证明了ZigZag（一种将BMC和k归纳结合在单个求解器中的算法）在向后执行时效率更高。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号