Patent ID: 6904590
Filing Date: 2005-06-07
Classification: G06F

Abstract:
1. A computer-implemented method for checking a model of a program, comprising: receiving a graph having a set of vertices and a successor function; initializing sets of path edges, sets of summary edges, and a work list; removing a vertex having a type from the work list; and analyzing the vertex based on the type so as to determine the reachability status of the vertex in the set of vertices, wherein analyzing includes updating a set of path edges associated with the vertex by using a transfer function associated with the vertex, wherein updating includes executing the following acts: receiving a vertex argument and a path edge argument, forming a union of the set of path edges associated with the vertex argument and the path edge argument if the path edge argument is not a subset of the set of path edges associated with the vertex argument, and inserting the vertex argument into the work list.