-
题名面向程序可达性验证的数组处理循环压缩方法
- 1
-
-
作者
许良晨
孟昭逸
黄文超
熊焰
-
机构
中国科学技术大学计算机科学与技术学院
安徽大学计算机科学与技术学院
-
出处
《信息网络安全》
CSCD
北大核心
2024年第3期374-384,共11页
-
基金
国家自然科学基金[62372422,61972369,62102385]
中央高校基本科研业务费专项资金[WK2150110024]
安徽省自然科学基金[2108085QF262]。
-
文摘
计算机软件的安全性和健壮性逐渐成为一个非常重要的问题,而自动软件形式化验证是一种验证软件程序安全性和健壮性的可靠性较高的方法。在自动软件形式化验证中,大规模数组和复杂循环导致状态爆炸,使得验证器无法在规定时间内完成验证,因此如何在保证验证正确性的前提下压缩数组规模是一个值得研究的课题。文章提出复杂循环等价类的定义和相关命题,并提出一种面向程序可达性验证的数组处理循环压缩方法,先利用控制流自动机和系统依赖图进行静态分析划分等价类,再根据循环依赖关系对等价类进行压缩,用压缩后程序的验证结果代替原始程序的验证结果。实验结果表明,文章提出的方法能够在保证验证正确性的前提下压缩程序的规模,提高验证效率。
-
关键词
等价类分析
软件形式化验证
静态分析
系统依赖图
-
Keywords
equivalence class analysis
software formal verification
static analysis
system dependency graph
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-