Patent ID: 7640536

Claim:
A method of verifying properties of a source program, the method comprising: creating a directed multigraph, using a processor, from the source program such that the directed multigraph includes vertices corresponding to variables within the source program, and such that the directed multigraph includes edges between the vertices corresponding to data dependencies between the variables, and wherein creating the directed multigraph from the source program such that it includes edges between the vertices corresponding to the data dependencies between the variables further comprises creating direct edges between vertices when there is a direct data dependency between corresponding variables, and creating delay edges between vertices when there is a delayed data dependency between corresponding variables; minimizing, using the processor, the directed multigraph, wherein minimizing the directed multigraph comprises identifying removable vertices in the directed multigraph, wherein to be identified as removable, a vertex in the directed multigraph must be identified as replaceable and must satisfy a condition of not having both an incoming delay edge and an outgoing delay edge; transforming the source program, using the processor, by inlining variables in the source program, based on the minimization of the directed multigraph, to produce a transformed program; and verifying properties of the transformed program, using the processor, using a model checking tool in order to verify the properties of the source program.