Integrating External Deduction Tools with ACL2 ∗ Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber Department of Computer Sciences University of Texas at Austin Austin, TX 78712, USA {kaufmann,moore,sandip,reeber}@cs.utexas.edu http://www.cs.utexas.edu/users/{kaufmann,moore,sandip,reeber} Abstract We present an interface connecting the ACL2 theorem prover with external de- duction tools. The logic of ACL2 contains several constructs intended to facilitate structuring of interactive proof development, which complicates the design of such an interface. We discuss some of these complexities and develop a precise specifica- tion of the requirements from external tools for sound connection with ACL2. We also develop constructs within ACL2 to enable the developers of external tools to satisfy our specifications. 1 Introduction Recent years have seen rapid advancement in the capacity of automatic reasoning tools, most notably for decidable theories such as propositional calculus and Presburger arith- metic. For instance, modern BDD packages and Boolean satisfiability solvers can auto- matically solve problems with tens of thousands of variables and have been successfully used to reason about commercial hardware system implementations. This advancement has sparked significant interest in the general-purpose, interactive theorem proving com- munity to improve the efficiency and automation in theorem provers by providing a connection with state-of-the-art automatic reasoning tools. In this paper, we present a general mechanism we are building to connect deduction tools, external to the ACL2 theorem prover, with that prover. ACL2 [KMM00, KM06] is an industrial-strength interactive theorem proving sys- tem. It consists of an efficient programming interface based on an applicative sub- set of Common Lisp [KM94], and a first-order, inductive theorem prover for a logic of recursive functions. The ACL2 theorem prover supports several deduction mech- anisms such as congruence-based conditional rewriting, well-founded induction, sev- eral decision procedures, and generalization. The theorem prover has been particu- larly successful in the verification of microprocessors and hardware designs such as ∗ This material is based upon work supported by DARPA and the National Science Foundation under Grant No. CNS-0429591, by the National Science Foundation under Grant No. ISS-0417413, and by DARPA under Contract No. NBCH30390004. the floating point multiplication, division, and square root algorithms of AMD proces- sors [MLK98, Rus98, RF00, FKR+ 02], microcode for the Motorola CAP DSP [BH97], separation properties for the Rockwell Collins AAMP7TM processor [GRW04], and a non-trivial pipelined machine with interrupts, exceptions, and speculative instruction execution [SH97]. However, the applicability of ACL2 (as in fact that of any theorem prover) is often limited by the amount of user expertise required to drive the theorem prover; indeed, the verification projects referenced above represent many man-years of effort. Yet, a significant number of lemmas proven in the process, in particular many proofs exhibiting invariance of predicates over executions of hardware design implemen- tations, can be expressed in a decidable theory and automatically dispatched by an automatic decision procedure for the theory. On the other hand, it is not trivial to connect ACL2 with an external deduction tool. The logic of ACL2 is complicated by the presence of several constructs intended to facili- tate effective proof structuring [KM01]. It is therefore imperative (i) to determine under what logical constraints a conjecture certified by a combination of the theorem prover and other tools can be claimed to be a valid theorem, and (ii) to provide mechanisms so that a tool implementor might be able to meet the logical constraints so determined. In this paper, we propose a general interface for connecting external tools with ACL2. The user can instruct ACL2 to use external deduction tools for reducing a goal formula C to a list of formulas LC during a proof attempt. The claim is that provability of each formula in LC implies the provability of C. We present a sufficient condition expressible in ACL2 guaranteeing this claim, and discuss the soundness requirements on the tool implementor. We also propose a modest augmentation of the logical guarantees provided by ACL2, in order to facilitate connection with certain types of tools (cf. Section 5). We distinguish between two classes of external tools, namely (i) tools verified by the ACL2 theorem prover, and (ii) unverified but trusted tools. A verified tool must be formalized in the logic of ACL2 and the sufficient condition alluded to above must be formally established by the theorem prover. An unverified tool can be defined using the ACL2 programming interface, and can invoke arbitrary executable programs using calls to the underlying operating system via a system call interface. An unverified tool is introduced with a “tag” acknowledging that the validity of the formulas proven using the tool depends on the correctness of the tool. The interface for unverified tools enables us to invoke Boolean Satisfiability solvers, BDD packages, etc., for simplifying ACL2 subgoals. Why might verified tools be of interest? The formal language of ACL2 is a programming language, based on an ap- plicative subset of Common Lisp. The close connection with Lisp makes it possible to write efficiently executable programs in the ACL2 logic [KM94]. In fact, most of the ACL2 source code is implemented in this language. We believe it will be handy to provide facilities to the ACL2 user to control proofs by (i) implementing customized domain-specific reasoning code, (ii) verifying with ACL2 that the code is sound, and (iii) invoking the code for proving theorems in the target domain. In fact, ACL2 cur- rently provides a way for users to augment its built-in term simplifier with their own customized reasoning code, via the so-called “meta rules” [BM81]. However, such rules essentially augment the reasoning engine of ACL2 without providing the user control to manipulate a specific subgoal arising during a proof. Furthermore, meta rules only allow reducing a term to one that is provably equivalent—they do not allow generalization. With our interface, an ACL2 user can invoke directly a customized, verified reasoning tool to replace a subgoal by a collection of possibly more general subgoals. The remainder of the paper is organized as follows. In Section 2 we provide a brief overview of the ACL2 system. In Sections 3 through 5 we present our interface for connecting verified and unverified external tools with ACL2, touching upon the logical underpinnings involved. We discuss related work in Section 6 and conclude in Section 7. No previous familiarity with ACL2 is assumed in this presentation; the relevant features of the logic and the theorem prover are discussed in Section 2. 2 ACL2 The name “ACL2” stands for “A Computational Logic for Applicative Common Lisp”. The name is used to denote (i) a programming language based on an applicative subset of Common Lisp, (ii) a first-order logic of recursive functions with induction, and (iii) a theorem prover for the logic. In this section, we provide a brief overview of ACL2. The review is not complete, but only intended to lay the foundation for our work. Readers interested in learning ACL2 are referred to the ACL2 Home Page [KM06] which contains extensive hypertext documentation together with references to several books and papers. 2.1 The logic The kernel of the ACL2 logic consists of a formal syntax, some rules of inference, and some axioms. Kaufmann and Moore [KM97] provide a precise description of the kernel logic. The logic supported by the theorem prover is an extension of the kernel logic. The kernel syntax describes terms composed of variables, constants, and function symbols applied to a fixed number of argument terms. The kernel logic introduces “for- mulas” as composed of equalities between terms and the usual propositional connectives. The syntax of ACL2 is the prefix-normal syntax of Lisp; thus, the application of a binary function f on arguments a and b is represented by (f a b) rather than the more traditional f (a, b). However, in this paper we will use the formal syntax only when it is relevant for the associated discussion. In particular we will write (x × y) instead of (* x y) and (if x then y else z) instead of (if x y z). The axioms of ACL2 describe the properties of certain Common Lisp primitives. For example, the following are axioms about the primitives equal and if: Axioms. x=y ⇒ equal(x, y) = T x 6= y ⇒ equal(x, y) = NIL x = NIL ⇒ (if x then y else z) = z x 6= NIL ⇒ (if x then y else z) = y Notice that the kernel syntax is quantifier-free and each formula is implicitly universally quantified over all the free variables in the formula. Furthermore, the use of function symbols equal and if make it possible to embed propositional calculus and equality into the term language. When we write a term τ in place of a formula, it stands for the formula τ 6= NIL. Thus, in ACL2, the following term is an axiom relating the Lisp functions cons, car, and equal. Axiom. equal(cons(car(x, y)), x) This axiom stands for the formula equal(car(cons(x, y)), x) 6= NIL, which is provably equivalent to car(cons(x, y)) = x. With this convention, we will feel free to interchange terms and formulas. We will similarly feel free to apply logical connectives to a term or formula. Thus when we write ¬τ , where τ is a term, we mean the term (or formula by the above convention) obtained by applying the function symbol not to τ , where not is axiomatized as: Axiom. not(x) = if x then NIL else T The convention above enables us to interpret an ACL2 theorem as follows. If the term τ (when interpreted as a formula) is a theorem then for all substitutions σ of free variables in τ to objects in the ACL2 universe the (ground) term τ /σ evaluates to a non-NIL value. This alternative view will be critical in deriving sufficient conditions for correctness of external tools integrated with ACL2. The kernel logic includes axioms that characterize the primitive Lisp functions over numbers, characters, strings, symbols, and ordered pairs. These objects together make up the ACL2 standard universe; but “non-standard” ACL2 universes may contain other objects. Lists are represented as ordered pairs, so that the list (1 2 3) is represented as cons(1, cons(2, cons(3, NIL))). For brevity, we will write list(x, y, z) as an abbrevia- tion for cons(x, cons(y, cons(z, NIL))). Another convenient data structure built out of ordered pairs is the association list (or alist) which is essentially a list of pairs, e.g., list(cons("a", 1), cons("b", 2)). We often use alists for describing finite mappings; the above alist can be thought as a mapping that associates the strings "a" and "b" with 1 and 2, respectively. In addition to propositional calculus and equality the rules of inference of ACL2 in- clude instantiation, together with first-order induction over 0 (see below). For instance, the formula car(cons(2, x)) = 2 is provable by instantiation from the above axiom relat- ing car, cons, and equal. The ACL2 theorem prover initializes with a boot-strapping (first-order) theory called the Ground Zero theory (GZ for short). In the sequel, whenever we mention an ACL2 theory, we mean a theory obtained by extending GZ via the extension principles ex- plained below. The theory GZ contains the axioms of the kernel logic. In addition, it also contains a well-founded first-order induction principle, by way of an embedding of ordinals below 0 . In particular, GZ is assumed to be inductively complete, that is, it is assumed implicitly to contain all the first-order well-founded induction axioms expressible using formulas φ in the language of GZ: (∀y < 0 )[((∀x < y)φ/{y := x}) ⇒ φ(y)] ⇒ (∀y < 0 )φ(y) 2.1.1 Extension Principles ACL2 also provides several extension principles that allow the user to extend a theory by introducing new function symbols and axioms about them. Two extension principles that are particularly relevant to us are (i) the definitional principle to introduce total functions, and (ii) the encapsulation principle to introduce constrained functions,1 and we discuss them in some detail. Note that whenever we say (below) that a theory is extended by axiomatizing new function symbols we implicitly assume that the resulting theory is also inductively complete, that is, all the induction axioms in the language of the extended theory are also introduced together with the axioms explicitly specified. Definitional Principle: The definitional principle allows the user to extend a theory by axiomatizing new total (recursive) functions. For example, one can use this principle to introduce the unary function symbol fact axiomatized as follows, which returns the factorial of its argument. Definitional Axiom. fact(n) = if natp(n) ∧ (n > 0) then n × fact(n − 1) else 1 Here, natp(n) is axiomatized in GZ to return T if n is a natural number, and NIL otherwise. To ensure that the extended theory is consistent, ACL2 first proves that the recursion terminates. This is achieved by exhibiting some measure m that maps the set of function arguments to some well-founded structure derived from the embedding of ordinals below 0 . For the axiom above, an appropriate measure is nfix(n) which is axiomatized in GZ to return n if n is a natural number, otherwise 0. Encapsulation Principle: The encapsulation principle allows the extension of the ACL2 logic with functions intro- duced with constraints rather than full definitions. This principle, for instance, allows us to extend a theory by introducing a new unary function foo with only the following axiom that merely posits that foo always returns a natural number: Encapsulation Axiom. natp(foo(x)) The encapsulation axioms are also referred to as constraints, and the functions intro- duced via this principle are called constrained functions. To ensure the consistency of the resulting theory, one must show that there exist (total) functions satisfying the al- leged constraints; such functions are called witnesses to the constraints. For foo above, an appropriate witness is the constant function that always returns 1. For a constrained function f the only axioms known are the constraints. Therefore, any theorem proved about f is also valid for a function f 0 that also satisfies the con- straints. More precisely, call the conjunction of the constraints on f the formula φ. For any formula θ, let θ0 be the formula obtained by replacing the function symbol f by the function symbol f 0 . Then a derived rule of inference, functional instantiation, specifies that if φ0 and ψ are theorems then ψ 0 is also a theorem. Consider, for example, the con- stant function of one argument that returns 10. This function satisfies the constraint for foo; thus if bar(foo(x)) is provable for some function bar then functional instantiation can be used to prove bar(10). . 1 Other extension principles include the introduction of Skolem (choice) functions and specification of a formula as an axiom. The latter is discouraged since one can introduce unsoundness by adding arbitrary axioms. For this paper, we will ignore the possibility of introducing arbitrary axioms. 2.2 The Theorem Prover As a theorem prover, ACL2 is an automated, interactive proof assistant. It is automated in the sense that no user input is expected once the theorem prover has embarked on the search for the proof of a conjecture. It is interactive in the sense that the proof search is largely determined by the previously proven lemmas in its database at the beginning of a proof attempt; the user essentially programs the theorem prover by stating lemmas for it to prove, to use automatically in subsequent proofs. There is also a goal-directed interactive loop (called the “proof-checker”), similar in nature to what is offered by LCF-style provers; but it is much less frequently used and not relevant to the discussion below. Interacting with the ACL2 theorem prover principally proceeds as follows. The user creates a relevant theory (extending GZ) using the extension principles to model some artifact of interest. Then she poses some conjecture about the functions in the theory and instructs the theorem prover to prove the conjecture, possibly providing hints on how to proceed in the proof search. For instance, if the artifact is the factorial function above, an appropriate conjecture might be the following formula, which says that fact always returns a natural number. Theorem fact-is-natp: natp(fact(x)) = T The theorem prover attempts to prove such a conjecture by applying a sequence of transformations to it, replacing each goal (initially, the conjecture) with a list of sub- goals. ACL2 provides a hint mechanism that enables the user to instruct the theorem prover on how to proceed with its proof search at any goal or subgoal. For instance, the user can instruct the theorem prover to begin its proof search by inducting on x. Once a theorem is proven, the theorem prover stores it in a database, for use in subsequent derivations. This database groups theorems into various rule classes, which affects how the theorem prover will automatically apply them. The default rule class is rewrite, which causes the theorem prover to replace instances of the left-hand-side of an equality with its corresponding right-hand-side. If the conjecture fact-is-natp above is a rewrite rule, then subsequently whenever ACL2 encounters a term of the form natp(fact(τ )) in the course of a proof attempt, it rewrites the term to T. ACL2 users interact with the theorem prover primarily by issuing a sequence of event commands for introducing new functions and proving theorems with appropriate rule classes. For example, fact-is-natp is the name of the above theorem event. During proof development the user typically records events in a file, often referred to as a book. Once the desired theorems have been proven, the user instructs ACL2 to certify such a book in order to facilitate the use of the events in other projects. A book can be certified once and then included during a subsequent ACL2 session without rerunning the associated proofs. To facilitate structured proof development, the user is permitted to mark some of the events in a book as local events. For instance, to prove some relevant theorem the user might introduce several auxiliary functions and intermediate lemmas that are not generally useful; such events are typically marked to be local. When a book is included in a subsequent proof project, only the non-local events in the book are accessible, thus preventing unwanted clutter in the database of the theorem prover. The presence of local events complicates the soundness claims for ACL2. Note from above that local events in a book might include commands for introducing new functions (thus extending an ACL2 theory with new axioms), which are not available in the subsequent sessions where the book is loaded. Yet, in order to prove some non- local theorem in the book ACL2 might have used some of these local axioms. One must therefore answer under what condition it is legitimate to mark an axiomatic event in a book as local, and what formal soundness claims can be provided for an ACL2 session in which such a pre-certified book is loaded. Such questions have been answered by Kaufmann and Moore [KM01]: if a formula φ is proven as a theorem in an ACL2 session, then φ is in fact first-order derivable (with induction) from the axioms of GZ together with (hereditarily) only the axiomatic events in the session that involve the function symbols in φ. (In particular, every ACL2 session corresponds to a theory that is a conservative extension of GZ.) Thus, any definition or theorem that does not involve the function symbols in the non-local events of a book can be marked local. To implement this requirement, book certification involves two passes. In the first pass, ACL2 proves each theorem (and admits each axiomatic event) sequentially. In the second pass, it skips proofs, and makes a so-called local incompatibility check, checking primarily that each axiomatic event involved in any non-local theorem in the book is also non-local. 2.3 The ACL2 Programming Environment ACL2 is closely tied with Common Lisp. The formal syntax of the logic is essentially the syntax of Lisp, and the axioms in GZ for the primitive Lisp functions are carefully crafted so that the return value of a function as predicted by the axioms matches with the value specified in the Common Lisp Manual on arguments in the intended domain of its application. Furthermore, events corresponding to functions introduced using the definitional principle are essentially Lisp definitions. For instance, consider the factorial function fact described above. The formal event introducing the definitional axiom of fact is written in ACL2 as follows. (defun fact (n) (if (and (natp n) (> n 0)) (* n (fact (- n 1))) 1)) This is essentially a Lisp definition of the function! The connection with Common Lisp enables the users of ACL2 to execute formal definitions by using the underlying Lisp evaluator. Since Lisp is an ANSI-standard, efficient functional programming language, ACL2 users often make use of the connection to implement formally defined yet efficient code. Indeed, the theorem prover itself makes use of this connection for simplifying ground terms during proof search; for instance, ACL2 will simplify fact(3) to 6 by evaluation in the underlying Lisp. In order to facilitate efficient code development, ACL2 also provides a logic-free programming environment. A user can implement any applicative Lisp function and mark it to be in program mode. No proof obligation is generated for such functions. ACL2 can evaluate such functions using the Lisp evaluator, although no logical guarantee (including termination) is provided. Furthermore, ACL2 provides an interface to the underlying operating system, which enables the user to invoke arbitrary executable code (and operating system commands) from inside an ACL2 session. 2.4 Evaluators ACL2 provides a convenient notation for defining an evaluator for a fixed set of functions. Evaluators are used to support meta reasoning [BM81]. We will not consider meta reasoning in this paper, but we briefly mention evaluators since they will be useful in characterizing the correctness of external tools. A proof search involves applying transformations to reduce a goal to a collection of subgoals. Internally, ACL2 stores each goal as a clause represented as an object in the ACL2 universe. For instance, when ACL2 attempts to prove a theorem of the form τ1 ∧ τ2 ∧ . . . ∧ τn ⇒ τ , it represents the proof goal internally as a list of terms, (¬τ1 ... ¬τn τ ), which can be thought of as the disjunction of its elements (literals). When ACL2 works on any subgoal, the transformation procedures work on the internal representation of the subgoal, called the current clause. Since this representation is an ACL2 object, we can define functions over such objects. An evaluator makes explicit the connection between terms and their internal repre- sentations. Assume that f1 , . . . , fn are functions axiomatized in some ACL2 theory T . A function ev, also axiomatized in T is called an evaluator for f1 , . . . , fn , if the axioms associated with ev can be viewed as specifying an evaluation semantics for the internal representation of terms composed of f1 , . . . , fn that is consistent with the definitions of these functions; such axioms are then referred to as evaluator axioms. A precise char- acterization of all the evaluator axioms is described in the ACL2 Manual [KM06] under the documentation topic defevaluator; here we only mention one for illustration, which corresponds to the evaluation of the m-ary function symbol fi : An Evaluator Axiom. ev(list(0 fi ,0 τ1 , ...,0 τm ), a) = fi (ev(0 τ1 , a), . . . , ev(0 τm , a)) Here ’fi is assumed to be the internal representation of fi and ’τj is the internal representation of τj , for 1 ≤ j ≤ m. It is convenient to think of a as an association list that maps the (internal representation of the) free variables in τ1 , . . . , τm to ACL2 objects. Then the axiom specifies that the evaluation of the list (’fi ’τ1 ... ’τm ) (which corresponds to the internal representation of fi (τ1 , . . . , τm )) under some mapping of free variables to objects is the same as the function fi applied to the evaluation of each τj under the same mapping. 3 Verified External Tools In this section, we discuss verified external tools. We consider verified tools first since they are amenable to perhaps a simpler understanding than unverified ones. The ideas and infrastructure we develop in this section will be extended successively in the next two sections to support connections with unverified tools. We will refer to external deduction tools as clause processors. Recall that ACL2 internally represents terms as clauses, so that a subgoal of the form τ0 ∧ τ1 ∧ . . . ∧ τn ⇒ τ is represented as a disjunction by the list (¬τ0 ¬τ1 ... ¬τn τ ). Our interface enables the user to transform the current clause with custom code. More precisely, a clause processor is a function that takes a clause C (together with possibly other arguments) disjoin(C) = if ¬consp(C) then ∗NIL∗ else list(if, car(C), ∗T∗, disjoin(cdr(C))) conjoin(LC ) = if ¬consp(LC ) then ∗T∗ else list(if, disjoin(car(LC )), conjoin(cdr(LC )), ∗NIL∗) Figure 1: Axioms to support clause processors in GZ. Here *T* and *NIL* are assumed to be the internal representation of T and NIL respectively. The predicate consp is defined in GZ such that consp(x) returns T if x is an ordered pair, and NIL otherwise. and returns a list of clauses LC .2 The intention is that if each clause in LC is a theorem of the current ACL2 theory then so is C. In the remainder of the paper, when we talk about clause processors, we will mean such clause manipulation functions. Our interface for verified external tools constitutes the following components. • A new rule class for installing clause processors. Suppose the user has defined a function tool0 that she desires to use as a clause processor. She can then prove a specific theorem about tool0 (described below) and attach this rule class to the theorem. The effect is to install tool0 in the ACL2 database as a clause processor for use in subsequent proof attempts. • A new hint for using clause processors. Once tool0 has been installed as a clause processor it can be invoked via this hint to transform a conjecture during a sub- sequent proof attempt. If the user instructs ACL2 to use tool0 to help prove some goal G, then ACL2 transforms G into the collection of subgoals generated by executing tool0 on (the clause representation of) G. We now explain the theorem alluded to above for installing a function tool0 as a clause processor. Recall that one way to interpret a formula proven by ACL2 is via an evalu- ation semantics; that is, a formula Φ is a theorem if, for every substitution σ mapping each free variable of Φ to some object, Φ/σ does not evaluate to NIL. Our formal proof obligation for installing functions as clause processors is based on this evaluation se- mantics. Let C be a clause whose disjunction is the term τ , and let tool0, with C as its argument, produce the list (C1 ... Cn ) whose respective disjunctions are the terms τ1 , . . . , τn . Informally, we want to ensure that if τ /σ evaluates to NIL for some substitu- tion σ then there is some σ 0 and i such that τi /σ 0 also evaluates to NIL. This condition can be made precise in the logic of ACL2 by extending the notion of evaluators discussed in Section 2.4 from terms to clauses. Before describing the extension, we will assume that the ACL2 ground zero theory GZ contains two functions disjoin and conjoin axiom- atized as shown in Figure 1. Informally, the axioms specify how to interpret objects representing clauses and clause lists. For instance, the function disjoin specifies that the interpretation of a clause (τ0 τ1 τ2 ) is the same as the interpretation of (if τ0 T (if τ1 T (if τ2 T NIL)))), which represents the disjunctions of the terms τ0 , τ1 , and τ2 . Based on these axioms, we can formalize the correctness of clause processors by defining an evaluation semantics for clauses. In particular, assume that ev is an eval- uator for the single function if. Thus ev(list(if, τ0 , τ1 , τ2 ), a) stipulates how the term “if τ0 then τ1 else τ2 ” can be evaluated. For any theory T (obtained by extending GZ 2 The formal definition of a clause processor is somewhat more complex. In particular, it can optionally take as argument the current ACL2 state among others, and return, in addition to the list of clauses, an error message and possibly a new ACL2 state. We will ignore such details in this paper. term-listp(C) ∧ alistp(a) ∧ (ev(disjoin(C), a) = ∗NIL∗) ⇒ ev(conjoin(tool0(args, C)), tool0-env(args, C, a)) = ∗NIL∗ Figure 2: Correctness condition for clause processors. Here ev is assumed to be an evaluator for if, and args represents the remaining arguments of tool0 (in addition to clause C). The predicates term-listp and alistp are axiomatized in GZ such that (i) term-listp(x) returns a Boolean, which is T if and only if x is an object in the ACL2 universe representing a well-formed list of terms (and hence a clause), and (ii) alistp(a) returns a Boolean, which is T if and only if a is a well-formed association list. via the extension principles), a clause processor function tool0(args, C) will be said to be legal in T if there exists a function tool0-env in T such that the formula shown in Figure 2 is a theorem. The function tool0-env returns an association list like σ 0 in our in- formal example above: it potentially modifies the original association list to respect any generalization being performed by tool0. Note that a weaker theorem would logically suffice, replacing the use of the association list tool0-env(args, c, a) by an existentially quantified variable. A theorem of the form shown in Figure 2 can be tagged with the new rule class for clause processors, instructing ACL2 to use the function tool0 as a new verified external tool. Theorem 1 below, based on the “Essay on Correctness of Meta Reasoning” comment in the ACL2 sources, guarantees that the above condition is sufficient for the soundness of using tool0 to transform goal conjectures. Theorem 1 Let T be an ACL2 theory for which tool0 is a legal clause processor, and let tool0 return a list LC of clauses given an input clause C. If each clause in LC is provable in T , then C is also provable in T . Proof: The theorem is a simple consequence of the following lemma, given the correct- ness condition shown in Figure 2. Lemma 1 Let τ be a term with free variables v0 , . . . , vn , ev an evaluator for the function symbols in τ , and e a list of cons pairs of the form (h’v0, ’τ0 i ... h’vn, ’τn i), where ’vi and ’τi are internal representation of vi and τi respectively. Let σ be a substitution mapping each vi to τi , and let ’τ be the internal representation of the term τ . Then the following formula is a theorem: ev(0 τ , e) = τ /σ. Proof: An easy induction on the structure of term τ . The simplicity of the above proof might belie some of the subtleties involved. For instance, recall that each ACL2 theory T is a conservative extension of GZ. Furthermore, note that theorems whose proofs use an invocation of tool0 often do not involve the function symbols occurring in the definition of the function tool0 itself. For instance, assume that tool0 is a simple clause generalizer that replaces each occurrence of a specific subterm in a clause by a free variable not present in the original clause. Such a function can be invoked for generalization in the proof of a formula Φ although Φ might not contain any occurrence of tool0. On the completion of a successful proof of Φ, can we then mark tool0 as local? The answer is in general “no”, since Theorem 1 only guarantees provability of the clause input to the clause processor from those returned in the theory in which the clause processor is legal. In particular such a theory must contain the definitions of the function symbols being manipulated by tool0, and for this it suffices that tool0 not be marked local. In fact a soundness bug in a previous but very recent release of ACL2 occurred in an analogous context for meta rules, due to ACL2’s previous inability to track the fact that the theory in which such rules are applied indeed included the definitions supporting the corresponding evaluators. 4 Basic Unverified External Tools Verified clause processors are useful when the user intends to augment the reasoning engine of ACL2 with mechanically checked code for customized clause manipulation. However, more often, we want to manipulate goal conjectures using a tool that is external to the theorem prover, for instance a state-of-the-art Boolean satisfiability solver or model checker. In this section, we will consider an extension of the mechanisms to incorporate such tools. In the next section we will present additional constructs to facilitate integration with more general tools. Our interface for unverified tools involves extending the theorem prover with a new event that enables ACL2 to recognize some function tool1 defined by the user as an unverified clause processor. Here the function tool1 might be implemented using program mode and might also invoke arbitrary executable code using ACL2’s system call interface (cf. Section 2.3). The effect of the event in subsequent proof search with ACL2 is the same as if tool1 were introduced as a verified clause processor: hints can be used to invoke the function for manipulating terms arising during proofs. Suppose an unverified tool tool1 simplifies a clause in the course of proving some goal conjecture. What guarantees should an implementor of tool1 provide (and must the user trust) in order to claim that the goal conjecture is indeed a theorem? In this simple case, a sufficient guarantee is that there is a theory T containing the definition of tool1 and appropriate evaluators such that the formula analogous to the one shown in Figure 2 in the previous section for tool1 is a theorem of T . The soundness of the use of tool1 then follows from Theorem 1. Since the invocation of an unverified tool for simplifying ACL2 conjectures carries a logical burden, the event introducing such tools provides two constructs, namely (i) a tag for the user of the tool to acknowledge this burden, and (ii) a concept of supporters for the tool developer to implement the tool in a way as to be able to guarantee that the logical restrictions are met. We now explain these two constructs. The tag associated with an event installing an unverified tool tool1 is a symbol (the default value being the name of the tool itself), which must be used to acknowledge that the soundness of any theorem proven by an application of tool1 depends on the implementor of tool1 satisfying the logical guarantees above. The certification of any book that contains an event installing an unverified clause processor (or hereditarily includes such a book, even locally) requires the user to tag the certification command with the name of the tags introduced with the event. Note that technically the mere act of installing an unverified tool does not introduce any unsoundness; the logical burden expressed above pertains to the use of the tool. Nevertheless, our decision to insist that the certification of any book with an installation of an unverified tool (whether subse- quently used or not) to be tagged is governed by implementation convenience. Recall that the local incompatibility check (that is, the second pass of a book certification) skips proofs, and thereby ignores the hints provided during the proof process. By “tracking” the installation rather than the application of an unverified clause processor, we disallow the possibility of a user certifying a book that locally introduces an unverified tool and uses it for simplifying some formulas, without acknowledging the application of the tool. Finally we turn to supporters. This construct enables a tool developer to provide the guarantee outlined above in the presence of local events. To understand why this construct is necessary, consider the following scenario. Suppose a developer creates a book (say, book1) in which the function f is introduced locally with the following definitional axiom: Local Definitional Axiom. f (x) = x Suppose further that book1 also installs an unverified clause processor tool1. Assume that the definition of tool1 does not involve invocation of f , but it replaces terms of the form f (τ ) with τ ; thus the correctness of tool1 depends on the intended definition of f . However, if an ACL2 session is extended by including book1, then the extended session contains the definition of tool0 tagged as an unverified clause processor, but does not contain the (local) definition of f . Thus we can write another book (say, book2) that includes book1 and then provides a new definition of f , for instance the following: Definitional Axiom. f (x) = cons(x, x) We now are working in a theory in which tool1 may be used to perform term manipu- lations that are completely unjustified by the current definition of f , thus invalidating any guarantee provided by the implementor of tool1. In general, then, suppose that a tool has built-in knowledge about some function symbols. The tool implementor cannot meet the logical burden expressed above un- less the user of the tool is required to include the axioms that have been introduced for those function symbols. The supporters construct of the event installing unverified clause processors provides a way for the implementor to insist that such axioms are present, by listing the names of axiomatic events (typically function symbols that name their definitions, e.g., f in the example above). We will refer to these events as the sup- porting events for the clause processor. Whenever ACL2 encounters an event installing a function tool1 as an unverified clause processor with a non-empty list of supporters, it will check that tool1 and all of the supporting event names are already defined. 5 Templates and Generalized External Tools The view above of unverified tools is that if a clause processor replaces some clause with a list of clauses then the provability of the resulting clauses implies the provability of the original clause. A clause processor is thus an efficient procedure for assisting in proofs of theorems that could, in principle, have been proven from the axiomatic events of the current theory. This simple view is sufficient in most situations; for instance, one can use it to connect ACL2 with a Boolean satisfiability solver that checks if a propositional formula is a tautology. However, some ACL2 users have found the necessity to use more sophisticated tools that implement their own theory. We will now discuss an extension to the ACL2 logic that facilitates connection with such tools. To motivate the need for such tools, assume that we wish to prove a theorem about some hardware design. Most such designs are written in a Hardware Description Lan- guage (HDL) such as VHDL or Verilog. One way of formalizing such designs is to define a semantics of the HDL in ACL2, possibly by defining a formal interpreter for the language. However, defining such an interpreter is typically extremely complex and labor-intensive. On the other hand, there are several model checkers available which can parse designs written in VHDL or Verilog. An alternative is merely to constrain some properties of the interpreter and use a combination of theorem proving and model checking in the following manner: • Establish low-level properties of parts of a design using model checkers or other decision procedures. • Use the theorem prover to compose the properties proven by the model checker together with the constrained properties of the interpreter to establish the cor- rectness of the design. The above approach has shown promise in scaling formal verification to industrial de- signs. For instance, Sawada and Reeber [SR06] have recently verified an industrial VHDL floating-point multiplier using a combination of ACL2 and an IBM internal ver- ification tool called SixthSense [MBP+ 04]. They introduce two functions, sigbit and sigvec, with the following assumed semantics: • sigbit(e, s, n, p) returns a bit corresponding to the value of bit signal s of a VHDL design e at cycle n and phase p. • sigvec(e, s, l, h, n, p) returns a bit vector corresponding to the bit-range between l and h of s for design e at cycle n and phase p. In ACL2 these two functions are constrained only to return a bit and bit-vector respec- tively. The key properties of the different multiplier stages are proven using SixthSense. For instance, one of the properties proven is that sigvec when applied to (i) a constant C representing the multiplier design, (ii) a specific signal s of the design, (iii) two spe- cific values lb and hb corresponding to the bit-width of s, and (iv) a specific cycle and phase, returns the sum of two other bit vectors at the previous cycle; this corresponds to one stage of the Wallace-tree decomposition implemented by the multiplier. All such theorems are then composed by ACL2 to verify that the multiplier, when provided two vectors of the right size, produces their product after 5 cycles. How do we support this verification approach? Note that the property above is not provable from the constraints on the associated functions alone (namely sigvec returns a bit vector). Thus if we use encapsulation to constrain sigvec and posit the property as a theorem then functional instantiation can derive an inconsistency. The problem is that the property is provable from the constraints together with axioms about sigvec that are unknown to ACL2 but assumed to be accessible to SixthSense. Our solution to the above is to extend the extension principles of ACL2 with a new principle called encapsulation templates (or simply templates). Function symbols introduced via templates are constrained functions just like those introduced via the encapsulation principle, and the soundness of extending an ACL2 theory is analogously guaranteed by exhibiting a local witness satisfying the constraints. However, there is one significant distinction between encapsulation principle and templates: the constraints introduced are marked incomplete, acknowledging that they might not encompass all the constraints on the functions. ACL2 therefore disallows functional instantiation of theorems by substituting for functions introduced via templates. The use of template events facilitates integration of ACL2 with tools like SixthSense above. Suppose that we wish to connect ACL2 with an unverified tool tool1 that im- plements a theory that we do not wish to define explicitly in ACL2. We then use a template event to introduce the function symbols (say f and g) regarding which the theory of the clause processor contains additional axioms. Finally we introduce tool1 as an unverified clause processor, marking f and g as supporting events. We now explain the logical burden for the developer of such a connection. Assume that an ACL2 theory T is extended by a template event E, and suppose that the supporting events for tool1 mention some function introduced by E. Then the developer of tool1 must guarantee that it is possible, in principle, to introduce f and g via the encapsulation principle (which we will refer to as the “promised” encapsulation EP of the functions) such that the following conditions hold: 1. The constraints in EP include the constraints in E. 2. EP does not introduce any additional function symbols other than those intro- duced by E. 3. EP is admissible in theory T . 4. For any extension T0 of T together with the constraints in EP , if one can invoke tool1 to reduce some clause C to a list of clauses LC then if each clause of LC is first-order provable (with induction) in T0 then C must be provable in T0 . Furthermore, in order to make logical guarantees regarding ACL2 sessions that contain events corresponding to several unverified external tools, ACL2 enforces the following “disjointness condition”: a template event may not be extended to a promised encap- sulate by two different clause processors. Thus, when an unverified clause processor installation event has a supporting event name, f , such that f is a function symbol that had been introduced by a template, it is required that no unverified clause processor has been previously installed in the current ACL2 session that has a supporting event name that is a function symbol introduced in the same template. This makes it possible to view the event as essentially the (unique) promised encapsulation whose existence is guaranteed by the implementor of the tool. Note that condition 2 above is necessary for this purpose to preclude the possibility that the theory implemented by different external tools might have conflicting implicit axioms in their promised encapsulations for function symbols not introduced by the template. With these conditions, we can make the following informal claim for an ACL2 session which includes templates together with the use of unverified clause processors: Perform the following transformation in sequence to each template event E in the session. If there is a tool tool1 whose supporting events mention a function symbol introduced by E then replace E with the encapsulation EP promised by the developer of tool1. Otherwise extend E to an arbitrary admissible encapsulate. (Note that at least one such extension exists, namely one in which no additional constraint is introduced.) Then every alleged theorem in the session is in fact derivable in first-order logic (with induction) from the axiomatic events in the session produced after this transformation. The informal claim above can be made precise by formalizing the notion of an ACL2 session. Kaufmann and Moore [KM01] describe such a formalization where a valid session is modeled as a chronology, inductively defined as a sequence of events that is either (i) the empty sequence, or (ii) constructed from a sequence by introducing one of the legal ACL2 events such as commands for introducing new functions, and proving theorems. We omit that description here and refer the reader to their paper [KM01] for details. For this paper, we point out that given a careful inductive characterization of a session as a chronology, it is easy to see that an ACL2 session transformed as above really corresponds to a chronology. The basic observation is that for any chronology in which no function introduced by an encapsulation is functionally instantiated, the encapsulation may be strengthened and the result is still a chronology. The proof is by induction on the formation of chronologies, and each proof obligation encountered in the inductive step is discharged against the possibly stronger theory. 6 Related Work The importance of allowing the hooking up of external tools has been widely recognized in the theorem proving community. Some early ideas for connecting different theorem provers are discussed in a proposal for so-called “interface logics” [Gut91], with the goal to connect automated reasoning tools by defining a single logic L such that the logics of the individual tools can be viewed as sub-logics of L. More recently, with the success of model checkers and Boolean satisfiability solvers, there has been signifi- cant work connecting such tools with interactive theorem proving. The PVS theorem prover provides connections with several decision procedures such as model checkers and SAT solvers [RSS95, Sha01]. The Isabelle theorem prover [Pau] uses unverified external tools as oracles for checking formulas as theorems during a proof search; this mechanism has been used to integrate model checkers and arithmetic decision proce- dures with Isabelle [MN95, BF00]. Oracles are also used in the HOL family of higher order logic theorem provers [GM93]; for instance, the PROSPER project [DCN+ 00] uses the HOL98 theorem prover as a uniform and logically-based coordination mechanism between several verification tools. The most recent incarnation of this family of theo- rem provers, HOL4, uses an external oracle interface to decide large Boolean formulas through connections to state-of-the-art BDD and SAT-solving libraries [Gor02], and also uses that oracle interface to connect HOL4 with ACL2 as discussed in the next section. The primary basis for interfacing external tools with theorem provers for higher- order logic (specifically HOL and Isabelle) involves the concept of “theorem tagging”, introduced by Gunter for HOL90 [Gun98]. The idea is to introduce a tag in the logic for each oracle and view a theorem certified by the oracle as an implication with the tag corresponding to the certifying oracle as a hypothesis. This approach enables tracking of dependencies on unverified tools at the level of individual theorems. In contrast, our approach is designed to track such dependencies at the level of files, that is, ACL2 books. Our coarser level of tracking is at first glance unfortunate: if a book contains some events that depend on such tools and others that do not, then the entire book is “tainted” in the sense that its certification requires an appropriate acknowledgement for the tools. We believe that this will not prove to be an issue in practice, as ACL2 users typically find it easy to move events between books. On the positive side, it is simpler to track a single event introducing an external tool rather than uses of such an event, especially since hints are ignored when including previously certified books. As an aside, we note that a very general tagging mechanism is under development for ACL2, serving as a foundation in particular for tagging of unverified clause processors. There has also been work on using an external tool to search for a proof that can then be checked by the theorem prover without assistance from the tool. Hurd [Hur02] describes such an interface connecting HOL with first-order logic. McCune and Shum- sky [MS00] present a system called Ivy which uses Otter to search for first-order proofs of equational theories and then invokes ACL2 to check such proof objects. Meng and Paulson [MP04] interface Isabelle with a resolution theorem prover. Several ACL2 users have integrated external tools with ACL2; but without the disciplined mechanisms of this paper, such integration has essentially involved imple- mentation hacks on the ACL2 source code. Ray, Matthews, and Tuttle integrate ACL2 with SMV [RMT03]. Reeber and Hunt connect ACL2 with the Zchaff satisfiability solver [RH06], and Sawada and Reeber provide a connection with SixthSense [SR06]. Manolios and Srinivasan connect ACL2 with UCLID [MS04, MS05]. 7 Conclusion and Future Work Different deduction tools bring in different capabilities to formal verification. A strength of general purpose theorem provers compared to many tools based on decision procedures is in the expressive power of the logic, which enables succinct definitions. Automatic decision procedures provide more automated proof procedures for decidable theories. Several ACL2 users have requested ways to connect ACL2 with automated decision procedures. We believe that the mechanisms described in this paper will provide a dis- ciplined way of using ACL2 with other tools with a clear specification of the expectations from the tool in order to guarantee soundness of the ACL2 session. Furthermore, we believe that verified clause processors will provide a way for the user to control a proof more effectively without relying on ACL2’s heuristics. We have presented an approach to connecting ACL2 with external deduction tools, but we have merely scratched the surface. It is well-known that developing an effective interface between two or more deduction tools is a complicated exercise [KM92]. It remains to be seen how to effectively decompose theorem proving problems so as to make effective use of clause processors to provide the requisite automation. Some researchers have criticized our interface on the grounds that developing a con- nection with an external tool requires significant knowledge of the ACL2 logic. While we acknowledge that our interface requires understanding of that logic, including the term representation, we believe that such requirement is necessary for any developer interested in developing connections between formal tools. A connection between differ- ent formal tools must involve a connection between two logics, and the builder of such connection must understand both the logics, including the legal syntax of terms, and the axioms and rules of inferences. It should be noted that the logic of ACL2 is perhaps more complex than many others, principally because it offers proof structuring mecha- nisms by enabling the user to mark events as local. This complexity manifests itself in the interface; constructs such as supporters are provided essentially to enable the tool implementor to provide logical guarantees in the presence of local events. However, we believe that with these constructs it will be possible for the tool developers to implement connections with ACL2 with reasonable understanding of the theorem prover. Finally, note that the restrictions for the tool developers that we have outlined preclude certain external deduction tools. For instance, there has been recent work connecting HOL with ACL2 [GHKR06a, GHKR06b]; the approach there has been for a HOL user to make use of ACL2’s proof automation and fast execution capabilities. It might be of interest to the ACL2 user to take advantage of HOL’s expressive power as well. We are working on extending the logical foundations of ACL2 to facilitate such a connection. The key idea is that the ACL2 theorem prover might be viewed as a theorem prover for the HOL logic. If the view is accurate then it will be possible for the user of ACL2 to prove some formulas in HOL and use them in an ACL2 session, claiming that the session essentially reflects a HOL session mirrored in ACL2. Acknowledgements The authors thank Peter Dillinger, Robert Krug, Pete Manolios, John Matthews, and Rob Sumners for comments and feedback. References [BF00] D. Basin and S. Friedrich. Combining WS1S and HOL. In D. M. Gabbay and M. de Rijke, editors, Frontiers of Combining Systems 2, pages 39–56. Research Studies Press/Wiley, Baldock, Herts, UK, February 2000. [BH97] B. Brock and W. A. Hunt, Jr. Formally Specifying and Mechanically Ver- ifying Programs for the Motorola Complex Arithmetic Processor DSP. In Proceedings of the 1997 International Conference on Computer Design: VLSI in Computers & Processors (ICCD 1997), pages 31–36, Austin, TX, 1997. IEEE Computer Society Press. [BM81] R. S. Boyer and J S. Moore. Metafunctions: Proving them Correct and Using Them Efficiently as New Proof Procedure. In R. S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science. Academic Press, London, UK, 1981. [DCN+ 00] L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. F. Melham. The PROSPER toolkit. In S. Graf and M. Schwartbach, editors, Proceedings of the 6th International Conference on Tools and Algorithms for Constructing Systems (TACAS 2000), volume 1785 of LNCS, pages 78–92, Berlin, Germany, 2000. Springer-Verlag. [FKR+ 02] A. Flatau, M. Kaufmann, D. F. Reed, D. Russinoff, E. W. Smith, and R. Sumners. Formal Verification of Microprocessors at AMD. In M. Sheeran and T. F. Melham, editors, 4th International Workshop on Designing Cor- rect Circuits (DCC 2002), Grenoble, France, April 2002. [GHKR06a] M. J. C. Gordon, W. A. Hunt, Jr., M. Kaufmann, and J. Reynolds. An embedding of the ACL2 logic in HOL. In P. Manolios and M. Wilding, editors, 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006. [GHKR06b] M. J. C. Gordon, W. A. Hunt, Jr., M. Kaufmann, and J. Reynolds. An integration of HOL and ACL2. In A. Gupta and P. Manolios, editors, Proceedings of the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2006), San Jose, CA, November 2006. Springer-Verlag. [GM93] M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge Uni- versity Press, 1993. [Gor02] M. J. C. Gordon. Programming combinations of deduction and BDD- based symbolic calculation. LMS Journal of Computation and Mathemat- ics, 5:56–76, 2002. [GRW04] D. A. Greve, R. Richards, and M. Wilding. A Summary of Intrinsic Par- titioning Verification. In M. Kaufmann and J S. Moore, editors, 5th In- ternational Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004. [Gun98] E. L. Gunter. Adding External Decision Procedures to HOL90 Securely. Lecture Notes in Computer Science, 1479:143–152, 1998. [Gut91] J. D. Guttman. A Proposed Interface Logic for Verification Environments. Technical Report M-91-19, The Mitre Corporation, March 1991. [Hur02] J. Hurd. An LCF-Style Interface between HOL and First-Order Logic. In A. Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction (CADE 2002), volume 2392 of LNCS, pages 134–138. Springer-Verlag, 2002. [KM92] M. Kaufmann and J S. Moore. Should We Begin a Stanrdization Process for Interface Logics? Technical Report 72, Computational Logic Inc. (CLI), January 1992. [KM94] M. Kaufmann and J S. Moore. Design Goals of ACL2. Technical Report 101, Computational Logic Incorporated (CLI), 1717 West Sixth Street, Suite 290, Austin, TX 78703, 1994. [KM97] M. Kaufmann and J S. Moore. A Precise Description of the ACL2 Logic. See URL http://www.cs.utexas.edu/users/moore/- publications/km97.ps.gz, 1997. [KM01] M. Kaufmann and J S. Moore. Structured Theory Development for a Mechanized Logic. Journal of Automated Reasoning, 26(2):161–203, 2001. [KM06] M Kaufmann and J S. Moore. ACL2 home page, 2006. See URL http://- www.cs.utexas.edu/users/moore/acl2. [KMM00] M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston, MA, June 2000. [MBP+ 04] H. Mony, J. Baumgartner, V. Paruthi, R. Kanzelman, and A. Kuehlmann. Scalable Automated Verification via Exper-System Guided Transforma- tions. In A. J. Hu and A. K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004), volume 3312 of LNCS, pages 217–233. Springer-Verlag, 2004. [MLK98] J S. Moore, T. Lynch, and M. Kaufmann. A Mechanically Checked Proof of the Kernel of the AMD5K86 Floating-point Division Algorithm. IEEE Transactions on Computers, 47(9):913–926, September 1998. [MN95] O. Müller and T. Nipkow. Combining Model Checking and Deduction of I/O-Automata. In E. Brinksma, editor, Proceedings of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1995), volume 1019 of LNCS, Aarhus, Denmark, May 1995. Springer-Verlag. [MP04] J. Meng and L. C. Paulson. Experiments on Supporting Interactive Proof Using Resolution. In D. A. Basin and M. Rusinowitch, editors, Proceedings of the 2nd International Joint Conference on Computer-Aided Reasoning (IJCAR 2004), volume 3097 of LNCS, pages 372–384, 2004. [MS00] W. McCune and O. Shumsky. Ivy: A Preprocessor and Proof Checker for First-Order Logic. In P. Manlolios, M. Kaufmann, and J S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, pages 217–230. Kluwer Academic Publishers, Boston, MA, June 2000. [MS04] P. Manolios and S. Srinivasan. Automatic Verification of Safety and Live- ness of XScale-Like Processor Models Using WEB Refinements. In De- sign, Automation and Test in Europe (DATE 2004), pages 168–175, Paris, France, 2004. IEEE Computer Society Press. [MS05] P. Manolios and S. Srinivasan. Refinement Maps for Efficient Verification of Processor Models. In Design, Automation and Test in Europe (DATE 2005), pages 1304–1309, Munich, Germany, 2005. IEEE Computer Society Press. [Pau] L. Paulson. The Isabelle Reference Manual. See URL http://www.cl.- cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle2003/doc/ref.pdf. [RF00] D. Russinoff and A. Flatau. RTL Verification: A Floating Point Multiplier. In M. Kaufmann, P. Manolios, and J S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, pages 201–232, Boston, MA, June 2000. Kluwer Academic Publishers. [RH06] E. Reeber and W. A. Hunt, Jr. A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Computer-Aided Reasoning (IJCAR 2006), volume 4130 of LNAI, pages 453–467, 2006. [RMT03] S. Ray, J. Matthews, and M. Tuttle. Certifying Compositional Model Checking Algorithms in ACL2. In W. A. Hunt, Jr., M. Kaufmann, and J S. Moore, editors, 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003), Boulder, CO, July 2003. [RSS95] S. Rajan, N. Shankar, and M. K. Srivas. An Integration of Model-Checking with Automated Proof Checking. In P. Wolper, editor, Proceedings of the 8th International Conference on Computer-Aided Verification (CAV ’95), volume 939 of LNCS, pages 84–97. Springer-Verlag, 1995. [Rus98] D. Russinoff. A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD-K7 Floating-point Mul- tiplication, Division, and Square Root Instructions. LMS Journal of Com- putation and Mathematics, 1:148–200, December 1998. [SH97] J. Sawada and W. A. Hunt, Jr. Trace Table Based Approach for Pipelined Microprocessor Verification. In O. Grumberg, editor, Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997), volume 1254 of LNCS, pages 364–375. Springer-Verlag, 1997. [Sha01] N. Shankar. Using Decision Procedures with Higher Order Logics. In R. J. Boulton and P. B. Jackson, editors, Proceedings of the 14th International Conference on Theorem Proving in Higher-Order Logics (TPHOLS 2001), volume 2152 of LNCS, pages 5–26. Springer-Verlag, 2001. [SR06] J. Sawada and E. Reeber. ACL2SIX: A hint used to integrate a theorem prover and an automated verification tool. In A. Gupta and P. Manolios, editors, Proceedings of the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2006), San Jose, CA, November 2006. Springer-Verlag.