The patent badge is an abbreviated version of the USPTO patent document. The patent badge does contain a link to the full patent document.
The patent badge is an abbreviated version of the USPTO patent document. The patent badge covers the following: Patent number, Date patent was issued, Date patent was filed, Title of the patent, Applicant, Inventor, Assignee, Attorney firm, Primary examiner, Assistant examiner, CPCs, and Abstract. The patent badge does contain a link to the full patent document (in Adobe Acrobat format, aka pdf). To download or print any patent click here.
Patent No.:
Date of Patent:
Jan. 29, 2002
Filed:
Oct. 22, 1998
James B. Saxe, Palo Alto, CA (US);
Charles Gregory Nelson, Palo Alto, CA (US);
David Detlefs, Westford, MA (US);
Computer Computer Corporation, Houston, TX (US);
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.