An improved global analysis for program bug checking

Property simulation is an efficient approach that checks if a program satisfies certain temporal safety properties, and inter-procedural property simulation terminates in polynomial time and space. This paper first proposes a general framework for bug checking. Then, it defines function summary as a stand-in for the function. It improves property simulation and gives a new global analysis approach, in which the execution state is described in extended intervals. Experiments show that the testing tool based on this new approach has a higher accuracy rate for program bug checking.