【摘 要】
：
模型验证作为一种形式化技术,已逐渐应用于软件系统可靠性验证.但对结构复杂的大规模软件的验证,由于状态空间爆炸往往会导致验证过程效率低甚至失败.本文针对ANSI-C软件程序
【机 构】
：
大连理工大学 软件学院,辽宁省大连市 116620
论文部分内容阅读
模型验证作为一种形式化技术,已逐渐应用于软件系统可靠性验证.但对结构复杂的大规模软件的验证,由于状态空间爆炸往往会导致验证过程效率低甚至失败.本文针对ANSI-C软件程序的性质(正确性)验证问题,提出一种基于程序骨架的模型验证加速方法.该方法首先根据性质对源程序进行剪枝,并按照最大强连通分支压缩循环路径以抽取程序骨架,采用Hoare逻辑获取循环压缩节点的不变式,显著减小路径编码长度,将待验证性质转化为SMT一阶谓词逻辑公式,并采用SMT求解器Z3进行验证.实验结果表明抽取程序骨架后的验证效率有较大提升.
其他文献
目的:探讨临床护理路径在心血管专科疾病护理管理中的临床应用效果.方法:对我院心内科收治的心血管专科疾病患者分别进行常规护理和临床护理路径干预,观察并比较其护理效果.
高通量测序仪产生大量的DNA数据,FASTQ是存储DNA数据被广泛使用的数据格式.对FASTQ格式的数据进行压缩处理,能有效的节省存储空间.DSRC算法具有压缩比高的优点,因此对DSRC算
120汽油引起的慢性汽油中毒,对神经系统、血液系统等的影响已有许多报导,内分泌系统的改变也被国内许多学者注意。董士元发现石油制品可使甲状腺的功能状态发生障碍,同位素
异构加速部件在高性能计算中的广泛应用,给并行应用程序的开发提出了很大的挑战。OpeltACC编程标准旨在于制定一个基于编译指导命令的异构编程模型。本文基于开源软件accULL
针对模拟退火算法收敛速度慢、随机采样策略缺乏记忆能力、算法并行化问题依赖等缺点,利用粒子群优化(Particle Swarm Optimization,PSO)算法中的记忆功能引导算法在解空间开
关于异构架构需要重新检讨的一个普遍共识是:该平台仅适用于计算密集、热点突出类算法.这一“误解”来源于目前的主从协同模式,而非硬件架构.在传统的主从协同模式下,异构系
针对多核处理器系统中资源优化调度问题,提出了一种支持资源需求特征动态感知的资源适配框架A-SYS.A-SYS通过自适应控制处理器核资源分配量与任务资源需求特征相配,提升多核
目前已经提出了多种胖树路由算法,其中OSRM被证明是一种最优路由算法,但是所有算法都忽略了网络链路故障的易诊断性.为此,本文提出一种对OSRM改进的新型路由算法BT-OSRM.该算
桡骨远端骨折在临床上比较常见,一般情况下治疗的方法主要是先将其复位再使用石膏固定.但是这种治疗方法只是比较适合轻微骨折的患者,对于桡骨远端关节内粉碎性骨折的患者使
本文基于Reyhani-Masoleh提出的GF(2m)高斯正规基乘法实现了三拍非流水的正规基乘法器,并基于该乘法器实现了一种高性能López-Dahab标量乘硬件结构.Reyhani-Masoleh算法利用