期刊文献+
共找到17篇文章
< 1 >
每页显示 20 50 100
SMTLOC:基于多源频谱的SMT求解器缺陷定位
1
作者 王笑爽 周志德 +2 位作者 李晓晨 江贺 任志磊 《软件学报》 EI CSCD 北大核心 2024年第7期3314-3331,共18页
SMT求解器作为重要的基础软件,其存在的缺陷可能会导致依赖于它的软件功能失效,甚至带来安全事故.然而,修复SMT求解器缺陷是一个十分耗时的任务,因为开发者需要花费大量的时间和精力来理解并找到缺陷的根本原因.虽然已有许多软件缺陷定... SMT求解器作为重要的基础软件,其存在的缺陷可能会导致依赖于它的软件功能失效,甚至带来安全事故.然而,修复SMT求解器缺陷是一个十分耗时的任务,因为开发者需要花费大量的时间和精力来理解并找到缺陷的根本原因.虽然已有许多软件缺陷定位方面的研究,但尚未有系统的工作研究如何自动定位SMT求解器缺陷.因此,提出一种基于多源频谱的SMT求解器缺陷定位方法SMTLOC.首先,对于给定的SMT求解器缺陷,SMTLOC提出一种枚举算法,用以对触发该缺陷的公式进行变异,从而生成一组不触发缺陷,但与触发缺陷的公式具有相似执行路径的证人公式.然后,SMTLOC根据证人公式的执行路径以及SMT求解器的源码信息,提出一种融合覆盖频谱和历史频谱的文件可疑度计算方法,从而定位可能存在缺陷的文件.为了验证SMTLOC的有效性,收集60个SMT求解器缺陷.实验结果表明,SMTLOC的缺陷定位效果明显优于传统的频谱缺陷定位方法,SMTLOC可以将46.67%的缺陷定位在TOP-5的文件内,定位效果提升了133.33%. 展开更多
关键词 smt求解器 缺陷定位 覆盖频谱 历史频谱
下载PDF
基于SMT求解器的路径敏感程序验证 被引量:9
2
作者 何炎祥 吴伟 +1 位作者 陈勇 徐超 《软件学报》 EI CSCD 北大核心 2012年第10期2655-2664,共10页
随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损... 随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于SMT求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合F-Soft平台和Z3工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果. 展开更多
关键词 路径敏感 程序验证 抽象解释 符号执行 smt求解器
下载PDF
SMT求解技术简述 被引量:12
3
作者 金继伟 马菲菲 张健 《计算机科学与探索》 CSCD 北大核心 2015年第7期769-780,共12页
SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重... SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重介绍并分析了这些技术,包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点,包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望,量词的处理、优化问题和解空间大小的计算等尤其值得关注。 展开更多
关键词 可满足性模理论(smt) DPLL(T) 求解器
下载PDF
可满足性模理论综述
4
作者 唐傲 王晓峰 何飞 《计算机工程与科学》 CSCD 北大核心 2024年第3期400-415,共16页
可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广... 可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。 展开更多
关键词 一阶逻辑 可满足性模理论 Lazy方法 DPLL(T) smt求解器 #smt
下载PDF
SMT求解技术的发展及最新应用研究综述 被引量:10
5
作者 王翀 吕荫润 +2 位作者 陈力 王秀利 王永吉 《计算机研究与发展》 EI CSCD 北大核心 2017年第7期1405-1425,共21页
可满足性模理论(satisfiability modulo theories,SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(... 可满足性模理论(satisfiability modulo theories,SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考. 展开更多
关键词 可满足性模理论 smt求解器 smt求解算法 测试用例自动生成 程序缺陷检测 云计算
下载PDF
Spark环境下基于SMT的分布式限界模型检测
6
作者 任胜兵 张健威 +1 位作者 吴斌 王志健 《计算机工程》 CAS CSCD 北大核心 2017年第6期19-23,29,共6页
在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布... 在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示(LLVM-IR)构造为Spark内置的数据结构Pair RDD,利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集(VCs RDD),VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明,与传统串行检测方法相比,该方法提高了验证过程中的限界深度和验证结果的正确率,并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。 展开更多
关键词 软件验证 限界模型检测 弹性分布式数据集 可满足性模理论求解器 Spark框架
下载PDF
基于SMT求解器的微处理器指令验证数据约束生成技术 被引量:5
7
作者 谭坚 罗巧玲 +3 位作者 王丽一 胡夏晖 范昊 徐占 《计算机研究与发展》 EI CSCD 北大核心 2020年第12期2694-2702,共9页
处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory,SMT)的指令约束求解方法:利用可满足模理论求解器将指令级功能验证任务转化成数据约... 处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory,SMT)的指令约束求解方法:利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法:首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益. 展开更多
关键词 指令功能 数据路径 约束求解 smt求解器 验证数据 并行加速
下载PDF
SMT求解器理论组合技术研究 被引量:5
8
作者 李婧 刘万伟 《计算机工程与科学》 CSCD 北大核心 2011年第10期111-119,共9页
可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景。因此,本文重点介绍理论组合判定方法,概述... 可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景。因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术。通过对照实验,评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能。 展开更多
关键词 可满足模理论 smt求解器 组合理论
下载PDF
基于SMT求解器的BPEL过程数据流错误检测
9
作者 张成震 宋巍 +1 位作者 唐成宇 陈芳菲 《计算机工程与设计》 北大核心 2017年第12期3311-3315,共5页
针对现有检测数据流反模式错误方法常采用枚举策略,存在路径爆炸和异常误报等问题,提出一种基于可满足性模理论(SMT)约束求解器的符号编码去检测所有可行路径中的数据流反模式错误的方法。进行符号编码,包括最常见的3种数据流反模式,根... 针对现有检测数据流反模式错误方法常采用枚举策略,存在路径爆炸和异常误报等问题,提出一种基于可满足性模理论(SMT)约束求解器的符号编码去检测所有可行路径中的数据流反模式错误的方法。进行符号编码,包括最常见的3种数据流反模式,根据SMT约束求解器进行数据流反模式错误的识别检测。使用工业界中真实的BPEL过程作为数据集进行实验,实验结果表明,所提方法能够高效无误地检测出BPEL过程中的数据流异常错误。 展开更多
关键词 BPEL过程 数据流 反模式 符号编码 smt求解器
下载PDF
一种快速低内存消耗的SMT全解求解器
10
作者 白杨 贾悠 《通信技术》 2020年第7期1623-1629,共7页
SMT全解求解器为许多研究领域提供辅助,但现有的SMT全解求解器在速度、内存消耗或者支持的求解类型方面存在局限性。首先,提出了求解器的4种新的潜在应用;其次,设计了一种基于二分查找(Binary Search,BS)的新型求解器,可以支持多种求解... SMT全解求解器为许多研究领域提供辅助,但现有的SMT全解求解器在速度、内存消耗或者支持的求解类型方面存在局限性。首先,提出了求解器的4种新的潜在应用;其次,设计了一种基于二分查找(Binary Search,BS)的新型求解器,可以支持多种求解类型,同时,结合上下文感知(Context Aware,CA)机制来提升求解器的速度,并通过暂停恢复(Suspend Resume,SR)机制降低内存消耗。初步试验表明,BS、BS+CA、BS+SR和所提方法分别能将传统的阻塞子句方法(Blocking Clauses Method,BCM)的求解速度提高了4.6倍、13.4倍、7.3倍以及32.4倍;与BCM相比,提出的方案的内存消耗降低至35.3%。此外,试验结果表明,可以通过并行化进一步提升方案的性能。 展开更多
关键词 smt全解求解器 二分查找(BS) 上下文感知(CA) 暂停恢复(SR)
下载PDF
基于约束求解的城市轨道交通CBTC系统事件序列测试用例生成方法
11
作者 覃瑶 张亚东 +2 位作者 饶畅 段峰 郭进 《铁道科学与工程学报》 EI CAS CSCD 北大核心 2023年第9期3525-3535,共11页
城市轨道交通CBTC系统采用无线通信技术实现车−地连续双向、大容量信息传输。当前,我国正在大力发展自主化CBTC系统,为保障系统软件安全性,对系统进行信息交互测试是极为必要的。针对现有研究对CBTC系统的信息交互顺序测试不充分而引发... 城市轨道交通CBTC系统采用无线通信技术实现车−地连续双向、大容量信息传输。当前,我国正在大力发展自主化CBTC系统,为保障系统软件安全性,对系统进行信息交互测试是极为必要的。针对现有研究对CBTC系统的信息交互顺序测试不充分而引发的系统软件安全性问题,提出一种基于约束求解的事件序列测试用例生成方法。首先,根据系统蕴含的信息交互事件及其约束关系,提出一种基于事件索引的约束处理方法,实现顺序约束条件的1阶逻辑表示,继而采用约束求解器实现测试用例生成过程中的合法性校验及可扩展性校验。然后,基于贪心算法框架,提出事件序列测试用例的初始化、扩展与校验策略,实现事件序列测试用例集的高效精简生成。最后,以列车进站场景下的CBTC系统移动授权生成功能为研究对象,辨识各子系统间的信息交互事件、交互顺序及其约束,采用所提方法构建CBTC系统事件序列测试用例集。结果表明,所提方法可高效精简生成满足约束条件与覆盖准则的事件序列测试用例集,提高了测试的有效性与完备性。与穷举法相比,所提方法的测试用例集规模精简幅度可达到72.5%。与随机法相比,在生成相同规模的测试用例集时,所提方法的t-维事件序列覆盖率显著高于随机法,可在保证事件序列检错效力的前提下提高测试效率,从而为高效开展CBTC系统的信息交互顺序测试提供了理论依据。 展开更多
关键词 CBTC系统 事件序列测试 测试用例生成 smt求解器
下载PDF
基于可满足性模理论求解器的程序路径验证方法 被引量:2
12
作者 任胜兵 吴斌 +1 位作者 张健威 王志健 《计算机应用》 CSCD 北大核心 2016年第10期2806-2810,共5页
针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论(SMT)求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造... 针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论(SMT)求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造无循环控制流图(NLCFG);然后通过基本路径法对控制流图(CFG)进行遍历,提取基本路径信息;最后利用SMT求解器作为约束求解器,将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比,该方法在对测试集程序的验证时间上比CBMC降低了25%以上,比FSoft-SMT降低了15%以上;在验证精度上,该方法有明显的提升。实验结果表明,方法可以有效解决路径搜索空间过大的问题,同时提高路径验证的效率和准确率。 展开更多
关键词 路径验证 控制流图 决策树 基本路径 可满足性模理论求解器
下载PDF
数字微流控生物芯片调度算法
13
作者 郭继红 陈永利 《新乡学院学报》 2020年第9期50-53,73,共5页
数字微流控生物芯片技术是在芯片上集成生化过程中的反应、检测等功能,使芯片能自动完成实验分析的技术。实现了求解数字微流控生物芯片的液滴布局和调度问题的最优解算法。算法将芯片上液滴的移动、混合和检测等操作形式化为逻辑表达式... 数字微流控生物芯片技术是在芯片上集成生化过程中的反应、检测等功能,使芯片能自动完成实验分析的技术。实现了求解数字微流控生物芯片的液滴布局和调度问题的最优解算法。算法将芯片上液滴的移动、混合和检测等操作形式化为逻辑表达式,将表达式输入SMT求解器进行求解,得到液滴的布局和移动的最优解。 展开更多
关键词 微流控芯片 芯片实验室 smt求解器 布局和调度
下载PDF
Alzette的安全性分析 被引量:2
14
作者 许峥 李永强 王明生 《密码学报》 CSCD 2022年第4期698-708,共11页
本文研究了Alzette(2020年美密会议上提出的ARX结构S盒)抗差分类分析的安全性.首先,对于模加操作上的有效异或差分,通过利用符号差分的概念,本文给出了符号差分比特之间关系的比特向量表示.其次,通过将Lipmaa-Moriai限制条件以及符号差... 本文研究了Alzette(2020年美密会议上提出的ARX结构S盒)抗差分类分析的安全性.首先,对于模加操作上的有效异或差分,通过利用符号差分的概念,本文给出了符号差分比特之间关系的比特向量表示.其次,通过将Lipmaa-Moriai限制条件以及符号差分比特约束条件转化为SMT问题,本文提出了一种基于SAT/SMT求解器的ARX结构不可能差分区分器自动化搜索工具.该自动化工具是首个利用Lipmaa-Moriai限制条件以及符号差分搜索ARX结构不可能差分区分器的自动化工具.利用该工具可以发现被传统搜索方法忽略的有效的不可能差分区分器.最后,通过利用新的自动化工具以及传统方法搜索Alzette的不可能差分区分器,在输入差分汉明重量为2、输出差分汉明重量为1的条件下,我们分别发现了128993个和128767个不可能差分区分器,证明新的自动化工具能够更好地过滤无效差分路径;此外,将新的自动化搜索工具用于搜索4轮无密钥注入SPECK64不可能差分区分器,在输入差分汉明重量为2、输出差分汉明重量为1的条件下,我们发现了128976个不可能差分区分器,说明Alzette设计团队的安全性评估是不够全面的.据我们所知,这是首次利用不可能差分性质评估Alzette的安全性. 展开更多
关键词 Lipmaa-Moriai限制条件 符号差分 不可能差分 Alzette SAT/smt求解器
下载PDF
基于Z3的Coq自动证明策略的设计和实现 被引量:6
15
作者 张恒若 付明 《软件学报》 EI CSCD 北大核心 2017年第4期819-826,共8页
形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标... 形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减少了用户手动验证程序的开销. 展开更多
关键词 形式化验证 定理证明工具 约束求解器 COQ Z3
下载PDF
非交互式Petri网可覆盖性验证的高效实现 被引量:3
16
作者 丁如江 李国强 《软件学报》 EI CSCD 北大核心 2019年第7期1939-1952,共14页
近年来,基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中。然而,由于Petri网的可覆盖性问题复杂度太高,这类技术在应用时有较大的局限性,对于输入规模较大的问题常常会出现超时的情况。而Petri网的一个子系统非... 近年来,基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中。然而,由于Petri网的可覆盖性问题复杂度太高,这类技术在应用时有较大的局限性,对于输入规模较大的问题常常会出现超时的情况。而Petri网的一个子系统非交互式Petri网,其可覆盖性和可达性复杂性均是NP完备的,同时表达力又可以作为某类并发程序的验证模型。设计并实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV。采用基于约束的方法,从模型中提取约束,并使用Z3 SMT求解器对约束进行求解,同时,通过子网可标记方法对候选解进行验证,从而保证每组解都是正确解。通过实验分析了该工具的成功率、迭代次数以及运行效率,发现该算法不仅验证成功率高,而且性能非常优异。 展开更多
关键词 非交互式Petri网 可覆盖性 验证 模型检测 smt求解器
下载PDF
可满足模理论在软硬件划分领域的应用
17
作者 毛乐乐 胡小勤 卢晨 《广西民族大学学报(自然科学版)》 CAS 2016年第1期78-82,共5页
软硬件划分是评价软硬件协同设计优劣,甚至影响设计成败的关键技术之一.文章首次将可满足模理论应用于软硬件划分问题,借助Z3、CVC4与MathSAT5可满足问题解决器求得最优的软硬件划分方案,使得系统的软硬件实现代价最小,经实验验证,针对... 软硬件划分是评价软硬件协同设计优劣,甚至影响设计成败的关键技术之一.文章首次将可满足模理论应用于软硬件划分问题,借助Z3、CVC4与MathSAT5可满足问题解决器求得最优的软硬件划分方案,使得系统的软硬件实现代价最小,经实验验证,针对软硬件划分问题,Z3的综合性能要优于另外两种解决器.采用可满足性问题求解方案,不仅克服了传统启发式算法陷入局部最优解的弊端,同时也弥补了规划类算法不适应于大规模划分问题的不足. 展开更多
关键词 软硬件协同设计 软硬件划分 可满足模理论 可满足模理论求解器
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部