Array Processing Loop Compression Method for Program Reachability Verification
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.
equivalence class analysissoftware formal verificationstatic analysissystem dependency graph
NETL
NSTL
万方数据
