System and method for program verification and optimization

• US 6,343,376 B1
• Filed: 10/22/1998
• Issued: 01/29/2002
• Est. Priority Date: 10/22/1998
• Status: Expired due to Fees

• Current Assignee: Hewlett-Packard Development Company, L.P. (HP Inc.)
• Original Assignee: Computer Computer Corporation
• Inventors: Detlefs, David, Saxe, James B., Nelson, Charles Gregory
• Primary Examiner(s): Powell, Mark R.
• Assistant Examiner(s): INGBERG, TODD D
• Application Number:
  US09/176,950
• Time in Patent Office: 1,195 Days
• Field of Search: 717/4, 717/9, 717/5, 706/14, 706/18, 706/20, 706/382
• US Class Current: 717/154
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

A system and method for increasing the speed of operation of a theorem prover relating to program verification using adaptive pattern matching technique is disclosed. Source code in a specific programming language is converted to one or more formulae, each representing a specific reformulation of the source code that facilitates program verification. Each formula derived from the source code is converted into an E-graph which is a particular type of a directed acyclic graph having leaf nodes and interior nodes. Some of the nodes of an E-graph may be related to other nodes through equivalence relationships. Equivalence relationships between a group of nodes is stored in a data structure called an equivalence class. A collection of rules defining the grammar of the programming language is stored in an axiom database. Rules and conjectures can dynamically be added to the axiom database. Each rule or conjecture to be tested is converted into a pattern. The task of proving a rule or verifying some or all of the source code is transformed to the task of matching a pattern associated with the rule against the nodes of the E-graph. After each round of matching, the E-graph is modified by the addition of new equivalence relationships.

Claims

1. A computer-implemented method for verifying the conformity of information with one or more rules, said method comprising the steps of:

transforming the information into one or more formulae testable against one or more of the rules;

generating an initial graph from each of said formulae, each said graph including a directed acyclic graph connecting a plurality of nodes;

converting each of said one or more rules into one or more distinct search patterns;

searching each node of each said initial graph for instances of said distinct search pattern and storing each identified instance; and

repeating the following steps to thereby perform proving of the information as long as new instances of said one or more distinct search patterns are detected;

selectively modifying said graph;

identifying one or more regions of sad selectively modified graph as being relevant to a search for said one or more distinct search patterns; and

searching the nodes only in said identified relevant regions of said selectively modified graph for instances of said one or more distinct search patterns.

2. The computer-implemented method of claim 1 wherein a set of externally-generated rules about the syntax and semantics of the program or symbolic logic is created and modified dynamically.

3. The computer-implemented method of claim 1 for verifying the conformity of information with one or more rules, wherein the step of selectively modifying said graph is performed by adding new nodes to said graph.

4. The computer-implemented method of claim 1 for verifying the conformity of information with one or more rules, wherein the step of selectively modifying said graph is performed by activating previously inactive nodes in said graph.

5. The computer-implemented method of claim 1 for verifying the conformity of information with one or more rules, wherein the step of selectively modifying said graph is performed by adding equivalence relationships to selected nodes of said graph.

6. The computer-implemented method of claim 1 wherein said step of identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern is performed by maintaining information about the time at which each of the nodes in the active portion of said graph was last modified or affected.

7. The computer-implemented method of claim 6 wherein said information about the time at which each of the nodes in the active portion of said graph was last modified or affected is maintained by incorporating a status bit in a data structure associated with the nodes of the graph, said status bit being set when the associated node is modified during a round of matching and set status bit being cleared at the start of each round of matching.

8. The computer-implemented method of claim 6 in which at least one rule has been converted into multiple distinct search patterns (a “

multi-pattern”

), wherein information about the times at which each of the nodes in the active portion of said graph was last modified or affected is gated using the earliest modification time for all of the patterns of said multi-pattern.

9. A computer-implemented method for verifying the conformity of information with one or more rules, said method comprising the steps of:

transforming the information into one or more formulae testable against one or more of the rules;

generating an initial graph from each of said formulae, each said graph including a directed acyclic graph connecting a plurality of nodes;

converting each of said one or more rules into one or more distinct search patterns;

searching each node of each said initial graph for instances of said distinct search pattern and storing each identified instance; and

repeating the following steps to thereby perform proving of the information as long as new instances of said one or more distinct search patterns are detected;

selectively modifying said graph;

identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph; and

searching said selectively modified graph only for instances of said identified one or more relevant search patterns.

10. The computer-implemented method of claim 9 wherein a set of externally-generated rules about the syntax and semantics of the program or symbolic logic is created and modified dynamically.

11. The computer-implemented method of claim 9 for verifying the conformity of information with one or more rules, wherein the step of selectively modifying said graph is performed by adding new nodes to said graph.

12. The computer-implemented method of claim 9 for verifying the conformity of information with one or more rules, wherein the step of selectively modifying said graph is performed by activating previously inactive nodes to said graph.

13. The computer-implemented method of claim 9 for verifying the conformity of information with one or more rules, wherein the step of selectively modifying said graph is performed by adding equivalence relationships to selected nodes of said graph.

14. The computer-implemented method of claim 9 wherein said step of identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph is responsive to a merger of two or more equivalence classes.

15. The computer-implemented method of claim 14 wherein said step of identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to a merger of two or more equivalence classes further comprises the following steps:

determining a pair of function symbols, occurring in said distinct search pattern to he a parent-child pair, said parent-child pair of function symbols further comprising a parent function symbol and a child function symbol, said parent-child pair of function symbols being characterized by an application of said child function symbol also occurring as an argument of said parent function symbol in said distinct search pattern; and

detecting when said merger of two or more equivalence classes results in some active application of said child function symbol becoming equivalent to some active argument of said parent function symbol.

16. The computer-implemented method of claim 15 wherein said step of determining a pair of function symbols occurring in said distinct search pattern to be a parent-child pair is performed by maintaining a global set of parent-child pairs occurring in the active portion of said graph.

17. The computer-implemented method of claim 16 wherein said global set of parent-child function pairs is realized using an approximate set.

18. The computer-implemented method of claim 17 wherein said approximate set is implemented using a hash function.

19. The computer-implemented method of claim 14 wherein said step of identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to a merger of two or more equivalence classes further comprises the following steps:

determining a pair of function symbols, occurring in said distinct search pattern to be a parent-parent pair, said parent-parent pair of function symbols further comprising a first parent function symbol and a second parent function symbol, said parent-parent pair of function symbols being characterized by said first parent symbol and said second parent symbol being independently applied to two distinct occurrences of a common pattern variable in said distinct search pattern; and

detecting when said merger of two or more equivalence classes results in some active argument of said first parent function symbol becoming equivalent to some active argument of said second parent function symbol.

20. The computer-implemented method of claim 19 wherein said step of determining a pair of function symbols occurring in said distinct search pattern to be a parent-parent pair is performed by maintaining a global set of parent-parent pairs occurring in the active portion of said graph.

21. The computer-implemented method of claim 20 wherein said global set of parent-parent function pairs is realized using an approximate set.

22. The computer-implemented method of claim 21 wherein said approximate set is implemented using a hash function.

23. The computer-implemented method of claim 9 wherein said step of identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph is responsive to the activation of previously inactive nodes in said graph.

24. The computer-implemented method of claim 23 wherein said step of identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to the activation of previously inactive nodes in said graph further comprises the following steps:

updating a global set of parent-child pairs occurring in the active portion of said graph responsive to the activation of previously inactive nodes in said graph to include all parent-child pairs in the newly activated nodes;

updating a global set of parent-parent pairs occurring in the active portion of said graph responsive to the activation of previously inactive nodes in said graph to include all parent-parent pairs in the newly activated nodes; and

maintaining a global set of trivial parent elements occurring in the active portion of said graph and updating said global trivial parent set responsive to the activation of previously inactive nodes in said graph.

25. The computer-implemented method of claim 24 wherein said global set of trivial parent function elements is realized using an approximate set.

26. The computer-implemented method of claim 25 wherein said approximate set is implemented using a hash function.

27. The computer-implemented method of claim 9 wherein said step of identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph is responsive to the activation of new nodes in said graph.

28. The computer-implemented method of claim 27 wherein said step of identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to the activation of new nodes in said graph further comprises the following steps:

updating a global set of parent-child pairs occurring in the active portion of said graph responsive to the activation of new nodes in said graph to include all parent-child pairs in the newly activated nodes;

updating a global set of parent-parent pairs occurring in the active portion of said graph responsive to the activation of new nodes in said graph to include all parent-parent pairs in the newly activated nodes; and

maintaining a global set of trivial parent elements occurring in the active portion of said graph and updating said global trivial parent set responsive to the activation of new nodes in said graph.

29. The computer-implemented method of claim 28 wherein said global set of trivial parent function elements is realized using an approximate set.

30. The computer-implemented method of claim 29 wherein said approximate set is implemented using a hash function.

31. A computer-implemented system for verifying the conformity of information with one or more rules, said system comprising:

a verification condition generator for transforming at least a part of the information into one or more formulae that are amenable to automated testing against one or more of the rules;

a formula manager for generating an initial respective graph from each of said one or more formulae, each said graph including a directed acyclic graph connecting a plurality of nodes;

a pattern generator for converting each of said one or more rules into one or more distinct search patterns;

a prover for searching each node of each said initial graph for instances of said one or more distinct search patterns and storing each identified instance; and

iteration means to perform proving of the information as long as new instances of said one or more distinct search patterns are detected, including;

a graph modifier for selectively modifying said graph to add new nodes;

a relevance identifier for identifying one or more regions of said selectively modified graph as being relevant to a search for said one or more distinct search patterns; and

a pattern matcher for searching nodes only in said identified one or more relevant regions of said selectively modified graph for instances of said one or more distinct search patterns.

32. The computer-implemented system of claim 31 wherein a set of externally-generated rules about the syntax and semantics of the program or symbolic logic is created and modified dynamically.

33. The computer-implemented system of claim 31 for verifying the conformity of information with one or more rules, wherein said graph modifier for selectively modifying said graph adds new nodes to said graph.

34. The computer-implemented system of claim 31 for verifying the conformity of information with one or more rules, wherein said graph modifier for selectively modifying said graph activates previously inactive nodes of said graph.

35. The computer-implemented system of claim 31 for verifying the conformity of information with one or more rules, wherein said graph modifier for selectively modifying said graph adds equivalence relationships to selected nodes of said graph.

36. The computer-implemented system of claim 31 wherein the identification of one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern is performed by maintaining a modification time table containing information about the time at which each of the nodes in the active portion of said graph was last modified or affected.

37. The computer-implemented system of claim 36 wherein said information about the time at which each of the nodes in the active portion of said graph was last modified or affected is maintained by incorporating a status bit in a data structure associated with the nodes of the graph, said status bit being set when the associated node is modified during a round of matching and set status bit being cleared at the start of each round of matching.

38. The computer-implemented system of claim 36 in which at least one rule has been converted into multiple distinct search patterns (a “

multi-pattern”

), wherein information about the times at which each of the nodes in the active portion of said graph was last modified or affected is gated using the earliest modification time for all of the patterns of said multi-pattern.

39. A computer-implemented system for verifying the conformity of information with one or more rules, said system comprising:

a verification condition generator for transforming at least a part of the information into one or more formulae that are amenable to automated testing against one or more of the rules;

a formula manager for generating an initial respective graph from each of said one or more formulae, each said graph including a directed acyclic graph connecting a plurality of nodes;

a pattern generator for converting each of said one or more rules into one or more distinct search patterns;

a prover for searching each node of each said initial graph for instances of said one or more distinct search patterns and storing each identified instance; and

iteration means to perform proving of the information as long as new instances of said one or more distinct search patterns are detected, including;

a graph modifier for selectively modifying said graph;

a relevance identifier for identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph; and

a pattern matcher for searching said selectively modified graph only for instances of said identified one or more relevant search patterns.

40. The computer-implemented system of claim 39 wherein a set of externally-generated rules about the syntax and semantics of the program or symbolic logic is created and modified dynamically.

41. The computer-implemented system of claim 39 for verifying the conformity of information with one or more rules, wherein said graph modifier for selectively modifying said graph adds new nodes to said graph.

42. The computer-implemented system of claim 39 for verifying the conformity of information with one or more rules wherein said graph modifier for selectively modifying said graph activates previously inactive nodes of said graph.

43. The computer-implemented system of claim 39 for verifying the conformity of information with one or more rules, wherein said graph modifier for selectively modifying said graph adds equivalence relationships to selected nodes of said graph.

44. The computer-implemented system of claim 39 wherein said relevance identifier for identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph is responsive to a merger of two or more equivalence classes.

45. The computer-implemented system of claim 44 wherein said relevance identifier for identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to a merger of two or more equivalence classes further comprises the following:

a comparator means for determining a pair of function symbols, occurring in said distinct search pattern to be a parent-child pair, said parent-parent pair of function symbols further comprising a parent function symbol and a child function symbol, said parent-child pair of function symbols being characterized by an application of said child function symbol also occurring as an argument of said parent function symbol in said distinct search pattern; and

an equivalence detector for detecting when said merger of two or more equivalence classes results in some active application of said child function symbol becoming equivalent to some active argument of said parent function symbol.

46. The computer-implemented system of claim 45 wherein said comparator for determining a pair of function symbols occurring in said distinct search pattern to be a parent-child pair further comprises a database including a global set of parent-child pairs occurring in the active portion of said graph.

47. The computer-implemented system of claim 46 wherein said global set of parent-child function pairs is realized using an approximate set.

48. The computer-implemented system of claim 47 wherein said approximate set is implemented using a hash function.

49. The computer-implemented system of claim 44 wherein said relevance identifier for identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to a merger of two or more equivalence classes further comprises the following:

a comparator for determining a pair of function symbols, occurring in said distinct search pattern to be a parent-parent pair, said parent-parent pair of function symbols further comprising a first parent function symbol and a second parent function symbol, said parent-parent pair of function symbols being characterized by said first parent symbol and said second parent symbol being independently applied to two distinct occurrences of a common pattern variable in said distinct search pattern; and

an equivalence detector means for detecting when said merger of two or more equivalence classes results in some active argument of said first parent function symbol becoming equivalent to some active argument of said second parent function symbol.

50. The computer-implemented system of claim 49 wherein said comparator for determining a pair of function symbols occurring in said distinct search pattern to be a parent-parent pair further comprises a database including a global set of parent-parent pairs occurring in the active portion of said graph.

51. The computer-implemented system of claim 50 wherein said global set of parent-parent function pairs is realized using an approximate set.

52. The computer-implemented system of claim 51 wherein said approximate set is implemented using a hash function.

53. The computer-implemented system of claim 39 wherein said relevance identifier for identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph is responsive to the activation of previously inactive nodes in said graph.

54. The computer-implemented system of claim 53 wherein said relevance identifier for identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to the activation of previously inactive nodes in said graph further comprises the following:

a database updater for updating a global set of parent-child pairs occurring in the active portion of said graph responsive to the activation of previously inactive nodes in said graph to include all parent-child pairs in the newly activated nodes;

a database updater for updating a global set of parent-parent pairs occurring in the active portion of said graph responsive to the activation of previously inactive nodes in said graph to include all parent-parent pairs in the newly activated nodes; and

a database maintainer for maintaining a global set of trivial parent elements occurring in the active portion of said graph and updating said global trivial parent set responsive to the activation of previously inactive nodes in said graph.

55. The computer-implemented system of claim 54 wherein said global set of trivial parent function elements is realized using an approximate set.

56. The computer-implemented system of claim 55 wherein said approximate set is implemented using a hash function.

57. The computer-implemented system of claim 39 wherein said relevance identifier for identifying one or more search patterns as being relevant to the search for new matches being conducted in regions of said selectively modified graph is responsive to the activation of new nodes in said graph.

58. The computer-implemented system of claim 57 wherein said relevance identifier for identifying one or more regions of said selectively modified graph as being relevant to a search for a distinct search pattern responsive to the activation of new nodes in said graph further comprises the following:

a data base updater for updating a global set of parent-child pairs occurring in the active portion of said graph responsive to the activation of new nodes in said graph to include all parent-child pairs in the newly activated nodes;

a database updater for updating a global set of parent-parent pairs occurring in the active portion of said graph responsive to the activation of new nodes in said graph to include all parent-parent pairs in the newly activated nodes; and

a database maintainer for maintaining a global set of trivial parent elements occurring in the active portion of said graph and updating said global trivial parent set responsive to the activation of previously inactive nodes in said graph.

59. The computer-implemented system of claim 58 wherein said global set of trivial parent function elements is realized using an approximate set.

60. The computer-implemented system of claim 59 wherein said approximate set is implemented using a hash function.

61. A computer-implemented method for verifying the conformity of information with one or more rules, said method comprising the steps of:

transforming the information into one or more formulae testable against one or more of the rules;

generating an initial graph from each of said formulae, each said graph including a directed acyclic graph connecting a plurality of nodes;

converting each of said one or more rules into one or more distinct search patterns;

searching each node of each said initial graph for instances of said distinct search pattern and storing each identified instance; and

repeating the following steps to thereby perform proving of the information as long as new instances of said one or more distinct search patterns are detected;

selectively modifying said graph;

identifying one or more search patterns as being relevant to a search of said selectively modified graph for new matches;

identifying one or more regions of said selectively modified graph as being relevant to the search for new matches with said one or more relevant search patterns; and

searching the nodes only in said identified relevant regions of said selectively modified graph for instances only of said one or more relevant search patterns.

62. A computer-implemented method as in claim 61 wherein the selective modifying of said graph is performed recursively.

63. The computer-implemented method of clam 61 wherein the repeatedly performed proving is adaptive.

64. A computer-implemented system for verifying the conformity of information with one or more rules, said system comprising:

a verification condition generator configured for transforming at least a part of the information into one or more formulae that are amenable to automated testing against one or more of the rules;

a formula manager configured for generating an initial respective graph from each of said one or more formulae, each said graph including a directed acyclic graph connecting a plurality of nodes;

a pattern generator configured for converting each of said one or more rules into one or more distinct search patterns;

a prover for searching each node of each said initial graph for instances of said one or more distinct search patterns and storing each identified instance; and

iteration means to perform proving of the information as long as new instances of said one or more distinct search patterns are detected, including;

a graph modifier for selectively modifying said graph;

a relevance identifier configured for identifying one or more search patterns as being relevant to a search of said selectively modified graph for new matches and further configured for identifying one or more regions of said selectively modified graph as being relevant to the search for new matches with said one or more relevant search patterns; and

a pattern matcher configured for searching the nodes only in said identified relevant regions of said selectively modified graph for instances only of said one or more