Patent ID: 7844953

Claim:
A computer-readable storage medium storing a verification program that causes a computer to execute a process comprising: reading from a memory a first program and a second program to which the first program is altered by an alteration, the first program and the second program being a concurrent program or a parallel program; detecting a first function altered by the alteration, a second function using a shared variable influenced by the alteration, a first part having an altered part in the first function and an influenced part using the influenced shared variable in the second function, a control structure part relating to the control of processing by the first program and the second program, and a second part other than the first part and the control structure part in the first program and the second program, from the first program and the second program, according to a difference between the first program and the second program; generating a first model which is a finite state machine that represents the first program and a second model which is a finite state machine that represents the second program, the generating allocating each of basic blocks in the first part and the second part to a state in the first model and the second model and determining transitions in the first model and the second model according to the control structure part, each of the basic blocks having only one entrance and only one exit for a control flow; comparing the first model to the second model; verifying the second program by a trace process which searches whether a deadlock or a data race exists or not sequentially according to the state of determined transitions in the first model and the second model from an initial state (“determined transitions” is cited from generating step in previous paragraph as in bold); and displaying a result of the verifying on a display device.