【摘 要】
：
针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论（SMT）求解器的程序路径验证
【基金项目】
：
国家自然科学基金资助项目（61272151）,中南大学研究生自主探索创新项目（2016zzts374）.
论文部分内容阅读
针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论（SMT）求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造无循环控制流图（NLCFG）;然后通过基本路径法对控制流图（CFG）进行遍历,提取基本路径信息;最后利用SMT求解器作为约束求解器,将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比,该方法在对测试集程序的验证时间上比CBM
其他文献
病例1患者男，63岁。患者于1d前无明显诱因突然出现右口眼歪斜，当时无头痛、头晕、胸闷憋气及二便失禁等症，经休息后未缓解，遂就诊于天津市环湖医院，查颅脑MR示未见明显异常。2009
为解决连续属性值的离散化问题,提出了一种改进的自组织映射(SOM)聚类离散化算法,该算法利用SOM实现初始聚类,界定聚类上限;之后以初始聚类中心为样本,通过层次方法的平衡迭代规约和聚类(BIRCH)层次聚类算法进行二次聚类,解决聚类数虚高问题并确定离散断点集;最后对断点集任一样本找出其所在维各聚类中心的最近邻,以此作为离散微调依据。实验结果表明,该算法在断点集数(轮廓系数提升75%)及离散精度方面
针对现有基于混沌的医学图像加密算法的鲁棒性和效率不足,提出了一种基于快速混沌置乱的鲁棒型医学图像加密算法RMIEF-CS。算法利用两个低维的混沌系统交替迭代产生混沌序列,较好地解决了由于计算机精度有限而带来的混沌收敛问题;然后利用生成的混沌序列对图像明文数据流进行第一次置乱加密,对得到的密文采用新的混沌序列进行再次置乱得到最终密文。置乱过程中引入双向密文反馈机制增加算法的安全性和鲁棒性;算法利用低
针对虚拟专用网BGP/MPLS VPN技术原理,分析了边界网关协议(BGP)和多协议标签交换(MPLS)在OMNET++中的实现,进而基于OMNET++仿真环境提出了一套符合RFC标准的BGP/MPLS VPN的具体实现方案。最后给出了BGP/MPLS VPN的仿真实例的测试,验证了该方案的可行性。
三黄安神汤由刘方柏所创,主要由半夏秫米汤、僵蚕二黄汤及防己地黄汤组成.临床上主要用于痰火互结所致的失眠之证.随师治疗痰火扰心型失眠症一例,取得满意的疗效,现报道如下.
痛风是尿酸排泄减少，嘌呤代谢障碍，尿酸累积而致的疾病。患者以高尿酸血症、特征性急性关节炎、痛风结石形成为特点，严重者可致关节畸形及功能障碍或痛风性肾病。针对痛风不同临
标点符号的边界识别是自然语言处理的重要研究内容,它是分词、语块识别等应用的基础。为了实现中文中用于表示并列成分分割的顿号的边界识别,采用了用于序列分割和标记的条件随机场(CRF)方法进行顿号边界识别。首先对顿号边界识别任务进行了两种类型的描述,然后对顿号语料的标注方法和过程以及特征选择进行了研究,通过采用语料推荐和十折交叉验证两种数据集分配方法分别进行了边界识别实验。实验结果表明,通过条件随机场方