Data processing: software development – installation – and managem – Software program development tool – Translation of code
Reexamination Certificate
1998-10-22
2002-01-29
Powell, Mark R. (Department: 2122)
Data processing: software development, installation, and managem
Software program development tool
Translation of code
C717S152000, C706S014000, C706S018000, C706S020000, C706S032000
Reexamination Certificate
active
06343376
ABSTRACT:
TECHNICAL FIELD OF THE INVENTION
The invention relates to systems for program verification and automated theorem proving, and more particularly, to a static analysis technique for detecting errors in a software program.
DESCRIPTION OF RELATED ART
In the field of computer programming, it is often advantageous to check a software program statically, i.e., at compile-time, link-time or bind-time rather than at run-time. This enables a programmer to detect and correct certain types of errors prior to run-time, additionally saving the processing time and the consequences of running an erroneous program.
One of the techniques for static verification of a software program begins with a formula called a “verification condition” being derived from the program by a series of steps beginning typically with the parsing of the original program source code. A collection of terms occurring in the verification condition, optionally combined with a selected subset of terms occurring in an axiom set and terms derived from the verification condition or the axiom set is then represented by a particular kind of a directed acyclic graph (DAG) called an expression graph or E-graph. Such a static verification process ends with the analysis of the expressions in the E-graph using a set of rules. The rules define the ambit of the verification process and serve as the touchstone for measuring the correctness of a software program.
The analysis of the parsed expressions is conventionally performed using a set of rules reduces to the task of matching instances of various expressions in the E-graph against a set of prespecified patterns. This analysis is performed by a software program commonly referred to as a prover. Each of the prespecified patterns represent one or more rules. The instances of each of the patterns found in the E-graph is statically checked for formal correctness by the prover. As explored in greater detail elsewhere in this patent, the pattern-matching process that lies at the core of the prover becomes more complex in the presence of equalities.
Conventional provers, such as those used in prior program verification techniques, are often memory- and time-intensive because they use exhaustive search techniques. Furthermore, conventional provers do not generate adequate feedback when they fail to prove a conjecture, assertion or assumption. The lack of user-friendly reporting has reduced the usability and attractiveness of conventional provers.
It would therefore be desirable to have a prover that is both speedy as well as efficient in its use of memory resources. It would additionally be desirable to have a prover that could efficiently analyze a set of logical relationships to determine the truth or falsity of one or more assertions.
It has also been found desirable to have a prover analyze all or part of a computer program or other symbolic logical input using a set of formal rules that are themselves deduced from other parts of the program or input. The power and flexibility of a prover could be enhanced even further if it would accept user-supplied conjectures as well as internally generated working assumptions both statically as well as dynamically. It would additionally be useful to have a prover analyze computer source code or symbolic logical input using stored axioms from an axiom file or database.
It would be helpful if a prover were sensitive to the context of the analysis and distinguish between globally valid axioms, locally valid axioms and conditionally valid axioms. It would provide further utility if a prover used domain-specific algorithms for analyzing important functions and predicates such as arithmetic operators and the equality condition. It would be an added benefit if the pattern-matching techniques used in a prover were adaptable to other applications involving the matching of a graph against one or more patterns.
SUMMARY OF THE INVENTION
One of the principal problems addressed by the system and method of the present invention is to perform pattern matching (on an E-graph) in the presence of equalities. The system and method of the subject invention permits the prover input to be recursively-modified based upon prior prover output.
The present invention further aims at enhancing the power and flexibility of a prover by accepting user-supplied conjectures as well as internally-generated working assumptions both statically as well as dynamically. The present invention also provides further utility by using domain-specific algorithms for analyzing important functions and predicates such as arithmetic operators and the equality condition.
In one aspect, the present invention includes a technique for increasing the speed of operation of a theorem prover relating to program verification using adaptive pattern-matching. Source code in a specific programming language is converted to one or more formulae, each formula representing a specific reformulation of the source code that facilitates program verification. Each formula is converted into an E-graph which is a particular kind of a directed acyclic graph having leaf nodes and interior nodes connected by directed and/or undirected edges.
Certain of the formulae may be such that the E-graph associated with a formula may not be fully active for the purposes of the pattern-matching process. In the discussion that follows, the “active” portion of an E-graph refers to the part(s) of the E-graph over which the pattern matching process of the present invention executes. The pattern-matching process of the present invention is not performed on the “inactive” nodes of the E-graph. It should be emphasized that the set of “active” nodes of an E-graph can change dynamically during the operation of the present invention.
Some of the nodes of an E-graph (which are also referred to as E-nodes) may be related to other E-nodes through equivalence relationships. Equivalence relationships between groups of E-nodes are stored in a data structure which is referred to as an equivalence class. A collection of rules defining the semantics of the programming language is stored in an axiom database. Rules and conjectures about the source code may also be added to the axiom database during the analysis. Each rule and conjecture to be tested is first converted into a pattern.
The task of proving a rule or conjecture or verifying some or all of the source code is thus transformed into the task of matching the pattern associated with the rule or conjecture against the active nodes of the E-graph (i.e. the nodes corresponding to the appropriate portion of the source code). It should be noted that in the preferred embodiment of the present invention, the prover “proves” each rule or conjecture by attempting to disprove the negated rule or conjecture. In one implementation, this is done by combining the negated rule or conjecture with associated active portion of the E-graph into a data construct called the “context.” The prover attempts to disprove the negated rule or conjecture by looking for internal inconsistencies or contradictions in the constructed context.
The pattern-matching process at the core of the prover begins with a comprehensive search over the entire E-graph for the plenary set of patterns. This comprehensive baseline search is referred to as the first round of matching. After the initial round of matching, the E-graph may be modified by the addition of new nodes or equivalence relationships. The search for internal inconsistencies is repeated anew after each modification to the E-graph. These subsequent searches through the E-graph are referred to as Round 2 of matching, Round 3 of matching, etc. After each round of matching, the E-graph may be modified by the addition of new nodes or equivalence relationships or the activation of dormant nodes. It should be noted that an E-graph is typically invariant during a round of matching.
The efficiency of the pattern-matching process can be improved by limiting the search (using knowledge about the changes, if any, made to the E-graph after the previous round of matching) to only those po
Detlefs David
Nelson Charles Gregory
Saxe James B.
Computer Computer Corporation
Ingberg Todd
Oppenheimer Wolff & Donnelly LLP
Powell Mark R.
Sherry Leah
LandOfFree
System and method for program verification and optimization does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with System and method for program verification and optimization, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System and method for program verification and optimization will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2830347