Patent US6343376B1 successfully refreshed from Google Patents.
US6343376B1
Expired / Lapsed
US
⏱️ 0.0 years remaining
System and method for program verification and optimization
Assignee: Hewlett Packard Development Co LP
•
Filing: 1998-10-22
•
Granted: 2002-01-29
•
Expires: 2018-10-22
Abstract
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.
Inventors
- 👤 James B. Saxe
- 👤 Charles Gregory Nelson
- 👤 David Detlefs
Bibliographic Details
Application Number
—
Jurisdiction
US
Data Source
google_patents
Last Synchronized
2026-10-30 13:13
CPC Classifications
G; G06; G06F; G06F11/00; G06F11/36; G06F11/3604; G06F11/3608
Claims Analysis
Total Claims: 71
Claim 1
Independent Claim
173 words
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.
Claim 2
Dependent Claim
173 words
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.
Claim 3
Dependent Claim
28 words
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.
Claim 4
Dependent Claim
34 words
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.
Claim 5
Dependent Claim
35 words
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.
Claim 6
Dependent Claim
37 words
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.
Claim 7
Dependent Claim
57 words
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.
Claim 8
Dependent Claim
78 words
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.
Claim 9
Dependent Claim
60 words
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.
Claim 10
Dependent Claim
166 words
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.
Claim 11
Dependent Claim
166 words
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.
Claim 12
Dependent Claim
28 words
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.
Claim 13
Dependent Claim
34 words
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.
Claim 14
Dependent Claim
35 words
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.
Claim 15
Dependent Claim
37 words
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.
Claim 16
Dependent Claim
45 words
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.
Claim 17
Dependent Claim
143 words
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.
Claim 18
Dependent Claim
45 words
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.
Claim 19
Dependent Claim
20 words
The computer-implemented method of claim 16 wherein said global set of parent-child function pairs is realized using an approximate set.
Claim 20
Dependent Claim
16 words
The computer-implemented method of claim 17 wherein said approximate set is implemented using a hash function.
Claim 21
Dependent Claim
151 words
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.
Claim 22
Dependent Claim
45 words
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.
Claim 23
Dependent Claim
20 words
The computer-implemented method of claim 20 wherein said global set of parent-parent function pairs is realized using an approximate set.
Claim 24
Dependent Claim
16 words
The computer-implemented method of claim 21 wherein said approximate set is implemented using a hash function.
Claim 25
Dependent Claim
46 words
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.
Claim 26
Dependent Claim
154 words
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.
Claim 27
Dependent Claim
21 words
The computer-implemented method of claim 24 wherein said global set of trivial parent function elements is realized using an approximate set.
Claim 28
Dependent Claim
16 words
The computer-implemented method of claim 25 wherein said approximate set is implemented using a hash function.
Claim 29
Dependent Claim
45 words
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.
Claim 30
Dependent Claim
150 words
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.
Claim 31
Dependent Claim
21 words
The computer-implemented method of claim 28 wherein said global set of trivial parent function elements is realized using an approximate set.
Claim 32
Dependent Claim
16 words
The computer-implemented method of claim 29 wherein said approximate set is implemented using a hash function.
Claim 33
Dependent Claim
219 words
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.
Claim 34
Dependent Claim
219 words
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.
Claim 35
Dependent Claim
28 words
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.
Claim 36
Dependent Claim
32 words
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.
Claim 37
Dependent Claim
33 words
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.
Claim 38
Dependent Claim
35 words
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.
Claim 39
Dependent Claim
61 words
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.
Claim 40
Dependent Claim
78 words
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.
Claim 41
Dependent Claim
60 words
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.
Claim 42
Dependent Claim
206 words
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.
Claim 43
Dependent Claim
206 words
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.
Claim 44
Dependent Claim
28 words
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.
Claim 45
Dependent Claim
32 words
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.
Claim 46
Dependent Claim
33 words
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.
Claim 47
Dependent Claim
35 words
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.
Claim 48
Dependent Claim
46 words
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.
Claim 49
Dependent Claim
151 words
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.
Claim 50
Dependent Claim
46 words
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.
Claim 51
Dependent Claim
20 words
The computer-implemented system of claim 46 wherein said global set of parent-child function pairs is realized using an approximate set.
Claim 52
Dependent Claim
16 words
The computer-implemented system of claim 47 wherein said approximate set is implemented using a hash function.
Claim 53
Dependent Claim
159 words
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.
Claim 54
Dependent Claim
46 words
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.
Claim 55
Dependent Claim
20 words
The computer-implemented system of claim 50 wherein said global set of parent-parent function pairs is realized using an approximate set.
Claim 56
Dependent Claim
16 words
The computer-implemented system of claim 51 wherein said approximate set is implemented using a hash function.
Claim 57
Dependent Claim
47 words
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.
Claim 58
Dependent Claim
166 words
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.
Claim 59
Dependent Claim
21 words
The computer-implemented system of claim 54 wherein said global set of trivial parent function elements is realized using an approximate set.
Claim 60
Dependent Claim
16 words
The computer-implemented system of claim 55 wherein said approximate set is implemented using a hash function.
Claim 61
Dependent Claim
46 words
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.
Claim 62
Dependent Claim
164 words
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.
Claim 63
Dependent Claim
21 words
The computer-implemented system of claim 58 wherein said global set of trivial parent function elements is realized using an approximate set.
Claim 64
Dependent Claim
16 words
The computer-implemented system of claim 59 wherein said approximate set is implemented using a hash function.
Claim 65
Dependent Claim
197 words
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.
Claim 66
Dependent Claim
197 words
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.
Claim 67
Dependent Claim
17 words
A computer-implemented method as in claim 61 wherein the selective modifying of said graph is performed recursively.
Claim 68
Dependent Claim
13 words
The computer-implemented method of clam 61 wherein the repeatedly performed proving is adaptive.
Claim 69
Dependent Claim
13 words
The computer-implemented method of clam 61 wherein the repeatedly performed proving is adaptive.
Claim 70
Dependent Claim
243 words
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
Claim 71
Dependent Claim
243 words
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
References Cited (Backward Citations)
USPTO Annuity & Maintenance Windows
| Annuity Stage | Window Opens | Payment Deadline | Surcharge Period Until | Estimated Fee | Status |
|---|---|---|---|---|---|
| 3.5 Years (Year 4) | 2005-01-28 | 2005-07-30 | 2006-01-29 | $2000.00 | Window Closed / Lapsed |
| 7.5 Years (Year 8) | 2009-01-28 | 2009-07-30 | 2010-01-29 | $3760.00 | Window Closed / Lapsed |
| 11.5 Years (Year 12) | 2013-01-28 | 2013-07-30 | 2014-01-29 | $7700.00 | Window Closed / Lapsed |