排序方式： 共有3条查询结果，搜索用时 0 毫秒
1
1.
通过分析Krinke切片算法对程序循环体内嵌套一个或多个线程结构会产生切片不精确现象,得出Krinke算法所基于的程序依赖图对线程间数据的依赖关系定义得过于粗糙,且对并发程序执行行为的合法性约束不够严格的结果.据此,提出一种新的并发程序依赖图,引入跨线程边界循环-承载数据依赖关系,并在此数据结构上改进了切片算法;引入区域化执行证据概念,进一步约束程序执行行为的合法性,并给出了添加跨线程边界循环-承载数据依赖关系的算法及新的并发程序切片算法的伪代码.实例分析与算法性能测试表明,改进的切片算法克服了Krinke算法的不精确现象,降低了时间开销,改善了算法的可伸缩性. 相似文献
2.
针对软件模型检测中的状态爆炸问题，提出将程序条件化技术用于软件状态空间缩减的方案．以程序性质的线性时序逻辑公式可能出现的蕴涵式的前件作为条件化的约束条件，通过分析程序符号化执行语义，借助自动定理证明器，对语句的可达性条件进行逻辑推理，删除那些与性质的可满足性无关的语句，以达到程序精简的目的．理论分析和实验结果表明，条件化可以有效缩减程序状态空间，而且缩减后的程序模型保留了原程序中与所需验证的性质有关的所有信息，满足软件模型检测对状态缩减的安全性要求． 相似文献
3.
针对目前基于谓词抽象的程序模型检测工具很难处理大规模软件的现状，提出用过程提取技术对待检的源代码进行预处理，以改善程序模型检测的可伸缩性．首先，将程序中一个选定的语句集合提取出来并包装成一个独立的过程，然后在原程序的相应位置用一个过程调用替代，进而将大型程序分解成语义一致的小型过程的集合．由于模型检测算法中的过程总结边可单独计算，所以过程提取使整个程序的模型检测任务模块化，当程序对某过程进行多次调用时，利用总结边可以避免对过程体内状态空间的重复搜索，从而降低了模型检测算法在空间：和时间上的开销．理论分析和实验表明，所提技术能有效缩短大型程序的模型检测时间，并在程序的转换中不会改变原程序语义，满足了程序模型检测的安全性要求． 相似文献
1