This dissertation combines formal verification techniques in an attempt to reduce the human effort required to verify large systems formally. One method to reduce the human effort required by formal verification is to modify general-purpose theorem proving techniques to increase the number of lemma instances considered automatically. Such a modification to the forward chaining proof technique within the ACL2 theorem prover is described. This dissertation identifies a decidable subclass of the ACL2 logic, the Subclass of Unrollable List Formulas in ACL2 (SUFLA). SUFLA is shown to be decidable, i.e., there exists an algorithm that decides whether any SUFLA formula is valid. Theorems from first-order logic can be proven through a methodology that combines interactive theorem proving with a fully-automated solver for SUFLA formulas. This methodology has been applied to the verification of components of the TRIPS processor, a prototype processor designed and fabricated by the University of Texas and IBM. Also, a fully-automated procedure for the Satisfiability Modulo Theory (SMT) of bit vectors is implemented by combining a solver for SUFLA formulas with the ACL2 theorem prover's general-purpose rewriting proof technique. A new methodology for combining theorem proving and model checking is presented, which uses a unique "black-box" formalization of hardware designs. This methodology has been used to combine the ACL2 theorem prover with IBM's SixthSense model checker and applied to the verification of a high-performance industrial multiplier design. A general-purpose mechanism has been created for adding external tools to a general-purpose theorem prover. This mechanism, implemented in the ACL2 theorem prover, is capable of supporting the combination of ACL2 with both SixthSense and the SAT-based SUFLA solver. A new hardware description language, DE2, is described. DE2 has a number of unique features geared towards simplifying formal verification, including a relatively simple formal semantics, support for the description of circuit generators, and support for embedding non-functional constructs within a hardware design. The composition of these techniques extend our knowledge of the languages and logics needed for formal verification and should reduce the human effort required to verify large hardware circuit models.

Formal verification is becoming a critical tool for designing software and hardware today. Rising complexity, along with software's pervasiveness in the global economy have meant that errors are becoming more difficult to find and more costly to fix. Among the formal verification tools available today, theorem provers offer the ability to do the most complete verification of the most complex systems. However, theorem proving requires expert guidance and typically is too costly to be economical for all but the most mission critical systems. Three major challenges to using a theorem prover are: finding generalizations, choosing the right induction scheme, and generating lemmas. In this dissertation we study all three of these in the context of the ACL2 theorem prover. / text

Inference systems Τ and search strategies E for T are distinguished from proof procedures β = (T,E) The completeness of procedures is studied by studying separately the completeness of inference systems and of search strategies. Completeness proofs for resolution systems are obtained by the construction of semantic trees. These systems include minimal α-restricted binary resolution, minimal α-restricted M-clash resolution and maximal pseudo-clash resolution. Certain refinements of hyper-resolution systems with equality axioms are shown to be complete and equivalent to refinements of the pararmodulation method for dealing with equality. The completeness and efficiency of search strategies for theorem-proving problems is studied in sufficient generality to include the case of search strategies for path-search problems in graphs. The notion of theorem-proving problem is defined abstractly so as to be dual to that of and" or tree. Special attention is given to resolution problems and to search strategies which generate simpler before more complex proofs. For efficiency, a proof procedure (T,E) requires an efficient search strategy E as well as an inference system T which admits both simple proofs and relatively few redundant and irrelevant derivations. The theory of efficient proof procedures outlined here is applied to proving the increased efficiency of the usual method for deleting tautologies and subsumed clauses. Counter-examples are exhibited for both the completeness and efficiency of alternative methods for deleting subsumed clauses. The efficiency of resolution procedures is improved by replacing the single operation of resolving a clash by the two operations of generating factors of clauses and of resolving a clash of factors. Several factoring methods are investigated for completeness. Of these the m-factoring method is shown to be always more efficient than the Wos-Robinson method.

This thesis proposes improved methods for the automatic generation of proofs by structural induction in a formal system. The main application considered is proving properties of programs. The theorem-proving problem divides into two parts: (1) a formal system, and (2) proof generating methods. A formal system is presented which allows for a typed language; thus, abstract data types can be naturally defined in it. Its main feature is a general structural induction rule using a lexicographic ordering based on the substructure ordering induced by type definitions. The proof generating system is carefully introduced in order to convince of its consistency. It is meant to bring solutions to three problems. Firstly, it offers a method for generalizing only certain occurrences of a term in a theorem; this is achieved by associating generalization with the selection of induction variables. Secondly, it treats another generalization problem: that of terms occurring in the positions of arguments which vary within function definitions, besides recursion controlling arguments. The method is called indirect generalization, since it uses specialization as a means of attaining generalization. Thirdly, it presents a sound strategy for using the general induction rule which takes into account all induction subgoals, and for each of them, all induction hypotheses. Only then are the hypotheses retained and instantiated, or rejected altogether, according to their potential usefulness. The system also includes a search mechanism for counter-examples to conjectures, and a fast simplification algorithm.

This thesis describes a class of problems in which interactions occur when plans to achieve members of a set of simultaneous goals are concatenated in the hope of achieving the whole goal. They will be termed "interaction problems". Several well known problems fall into this class. Swapping the values of two computer registers is a typical example. A very simple 3 block problem is used to illustrate the interaction difficulty. It is used to describe how a simple method can be employed to derive enough information from an interaction which has occurred to allow problem solving to proceed effectively. The method used to detect interactions and derive information from them, allowing problem solving to be re-directed, relies on an analysis of the goal and subgoal structure being considered by the problem solver. This goal structure will be called the "approach" taken by the system. It specifies the order in which individual goals are being attempted and any precedence relationships between them (say because one goal is a precondition of an action to achieve another). We argue that the goal structure of a problem contains information which is simpler and more meaningful than the actual plan (sequence of actions) being considered. We then show how an analysis of the goal structure of a problem, and the correction of such a structure in the light of any interaction, can direct the search towards a successful solution. Interaction problems pose particular difficulties for most current problem solvers because they achieve each part of a composite goal independently and assume that the resulting plans can be concatenated to achieve the overall goal. This assumption is beneficial in that it can drastically reduce the search necessary in many problems. However, it does restrict the range of problems which can be tackled. The problem solver, INTERPLAN, to be described as a result of this investigation, also assumes that subgoals can be solved independently, but when an interaction is detected it performs an analysis of the goal structure of the problem to re-direct the search. INTERPLAN is an efficient system which allows the class of interaction problems to be coped with. INTERPLAN uses a data structure called a "ticklist" as the basis of its mechanism for keeping track of the search it performs. The ticklist allows a very simple method to be employed for detecting and correcting for interactions by providing a summary of the goal structure of the problem being tried.

Typescript. / Thesis (Ph. D.)--University of Hawaii at Manoa, 1977. / Bibliography: leaves 172-175. / Microfiche. / vii, 175 leaves ill

Thesis (Ph. D.)--University of Hawaii at Manoa, 1996. / Includes bibliographical references (leaves 140-144). / Microfiche. / x, 144 leaves, bound ill. 29 cm

Thesis (Ph. D.)--University of Texas at Austin, 2007. / Vita. Includes bibliographical references.

Thesis (Ph. D.)--University of Texas at Austin, 2008. / Vita. Includes bibliographical references.

Thesis (Ph.D.)--University of Western Australia, 2006.