增量式满足性检验算法在有界模型检验中的应用
151 浏览量
更新于2024-06-11
收藏 1.07MB PDF 举报
有界模型检验的增量式满足性检验算法及有效性验证
有界模型检验(Bounded Model Checking,BMC)是一种形式验证方法,用于检查模型是否满足一定的性质。该方法通过将模型转换为布尔可满足性(Satisfiability,SAT)问题来实现。然而,在BMC中,对长度递增的反例的搜索被转化为一系列满足性(SAT)检查。为提高搜索效率,需要开发出高效的搜索算法。
为解决该问题,本文提出了一种增量式满足性检验算法。该算法通过学习从一个实例转发在冲突分析期间学习的子句,尝试利用这些SAT实例的相似性来提高搜索效率。该算法分为两类:不注意生成SAT实例序列的机制的方法和那些依赖于它的方法。
在BMC运行的情况下,Strichman观察到,在一次SAT检查期间学习的那些仅依赖于模型结构的子句在检查更长的子句时仍然有效。E'en和Sorensson指出,如果翻译成SAT遵守通常遵循的规则,则可以转发所有已学习的子句许多条款,然而,以这种方式转发的数据几乎没有用处,并且可能降低性能。
本文提出了一个扩展斯特里奇曼的方法的形式,一个更一般的标准,以过滤冲突条款,可以有利地转发到连续的实例。这一标准,特别是,仍然是句法和相当有效的,但帐户的存在,主要和辅助目标的SAT实例。
此外,本文还介绍了一种技术,即使他们没有通过语法检查提取子句转发。蒸馏是一种语义方法,通常可以应用于增量SAT,并且经常产生独立于主要目标,因此对于实例序列的其余部分保持有效。此外,蒸馏通常可以提高子句的质量,即防止检查搜索空间的大区域的能力。
使用CirCU获得的实验结果SAT求解器确认了所提出的技术的有效性,特别是对于大的、困难的问题。
有界模型检验的增量式满足性检验算法的有效性验证是通过实验结果来确认的。实验结果表明,该算法可以提高搜索效率和解决问题的能力。此外,该算法还可以应用于其他形式验证方法,例如模型检查和形式验证等领域。
有界模型检验的增量式满足性检验算法是一种高效的搜索算法,可以应用于形式验证和模型检查等领域,以提高搜索效率和解决问题的能力。
2021-12-31 上传
论文
论文
论文
论文
论文
2023-05-11 上传
2023-05-20 上传
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 5
- 资源: 2万+
最新资源
- 多模态联合稀疏表示在视频目标跟踪中的应用
- Kubernetes资源管控与Gardener开源软件实践解析
- MPI集群监控与负载平衡策略
- 自动化PHP安全漏洞检测:静态代码分析与数据流方法
- 青苔数据CEO程永:技术生态与阿里云开放创新
- 制造业转型: HyperX引领企业上云策略
- 赵维五分享:航空工业电子采购上云实战与运维策略
- 单片机控制的LED点阵显示屏设计及其实现
- 驻云科技李俊涛:AI驱动的云上服务新趋势与挑战
- 6LoWPAN物联网边界路由器:设计与实现
- 猩便利工程师仲小玉:Terraform云资源管理最佳实践与团队协作
- 类差分度改进的互信息特征选择提升文本分类性能
- VERITAS与阿里云合作的混合云转型与数据保护方案
- 云制造中的生产线仿真模型设计与虚拟化研究
- 汪洋在PostgresChina2018分享:高可用 PostgreSQL 工具与架构设计
- 2018 PostgresChina大会:阿里云时空引擎Ganos在PostgreSQL中的创新应用与多模型存储