面向程序可达性验证的数组处理循环压缩方法

Array Processing Loop Compression Method for Program ReachabilityVerification

计算机软件的安全性和健壮性逐渐成为一个非常重要的问题,而自动软件形式化验证是一种验证软件程序安全性和健壮性的可靠性较高的方法。在自动软件形式化验证中,大规模数组和复杂循环导致状态爆炸,使得验证器无法在规定时间内完成验证,因此如何在保证验证正确性的前提下压缩数组规模是一个值得研究的课题。文章提出复杂循环等价类的定义和相关命题,并提出一种面向程序可达性验证的数组处理循环压缩方法,先利用控制流自动机和系统依赖图进行静态分析划分等价类,再根据循环依赖关系对等价类进行压缩,用压缩后程序的验证结果代替原始程序的验证结果。实验结果表明,文章提出的方法能够在保证验证正确性的前提下压缩程序的规模,提高验证效率。

The security and robustness of computer software have gradually become a very important issue in today's society,and automatic software formal verification is a highly reliable method to verify the security and robustness of software programs.However,in automatic software formal verification,large-scale arrays and complex loops lead to state explosion,making the verifier unable to complete verification within the specified time.Therefore,how to compress the array size while ensuring the correctness of verification is a subject worth to study.The article proposed the definition of complex loop equivalence classes and some propositions,and proposed an array processing loop compression method for program reachability verification.It first used control flow automata and system dependency graphs to perform static analysis to divide equivalence classes,and then divided equivalence classes according to loop dependencies compress equivalence classes and replaced the verification results of the original program with the verification results of the compressed program.Experiments show that the method proposed in this article can compress the size of the program and improve the verification efficiency while ensuring the correctness of verification.