Program Restructuring to Improve Efficiency of Software Model Checking

In order to cope with the problem, that is, the currently available software model checker can hardly deal with large-scale software, it is proposed to use the technique of program restructuring to pre-process the source code, so as to enhance the efficiency of software model checking. Program restructuring decomposes a large-scale program into a set of small procedures which preserves the original semantics. Due to the fact that the procedure summary edge can be separately computed in the model-checking algorithm, and a procedure may be called many times in a program, the pre-processing can avoid unnecessary repetition of state space search so as to decrease the overhead of space and the time in model checking algorithm. According to the components of linear temporal logic, the sufficient conditions for semantical equality of program restructuring are given. Given programs and programs property, the experimental results before and after restructuring the programs on the model checker “blast” are compared. Theoretical analysis and experimental results on some benchmark programs show that program restructuring can effectively decrease the overhead of model checking of large-scale programs, and at the same time, it can satisfy the security requirements of software model checking.