Scalable Techniques for Formal Verification
This book is about formal veri?cation, that is, the use of mathematical reasoning to ensure correct execution of computing systems. With the increasing use of c- puting systems in safety-critical and security-critical applications, it is becoming increasi
- PDF / 314,723 Bytes
- 25 Pages / 439 x 666 pts Page_size
- 101 Downloads / 255 Views
Introduction to ACL2
The name “ACL2” stands for A Computational Logic for Applicative Common Lisp. It is the name for (1) a programming language based on a subset of Common Lisp, (2) a logic, and (3) a mechanical theorem prover for the logic. ACL2 is an industrialstrength theorem prover that has been used successfully in a number of formal verification projects both in the industry and academia. As a logic, ACL2 is a firstorder logic of recursive functions with equality and induction. As a theorem prover, ACL2 is a complex software implementing a wide repertoire of heuristics and decision procedures aimed at effectively proving large and complicated theorems about mathematical artifacts and computing systems. The work in this monograph is based on the logic of ACL2, and all the theorems we claim to have mechanically verified have been derived using the ACL2 theorem prover. In this chapter, we present the logic of ACL2 and briefly touch upon how computing systems can be defined in ACL2 and how the logic can be used to prove theorems about them. To facilitate the understanding of the logic, we discuss its connections with traditional first-order logic. Readers interested in a more thorough understanding of ACL2 are referred to the ACL2 home page [124]. In addition, we list several books and papers about ACL2 in Sect. 3.8.
3.1 Basic Logic of ACL2 Recall from Chap. 2 that a formal logic consists of the following three components: A formal language for describing formulas A set of formulas called axioms A set of inference rules that allow derivation of new formulas from old.
As a logic, ACL2 is essentially a quantifier-free first-order logic of recursive functions with equality. Formulas are built out of terms, and terms are built out of constants, variables, and function symbols. More precisely, a term is either a constant, or a variable, or the application of an n-ary function symbol f on a list of n terms. The syntax of ACL2 is based on the prefix-normal syntax of Common Lisp. Thus, the application of f on arguments x1 ; : : : ; xn is represented S. Ray, Scalable Techniques for Formal Verification, DOI 10.1007/978-1-4419-5998-0 3, c Springer Science+Business Media, LLC 2010
25
26
3 Introduction to ACL2
as (f x1 : : : xn ) instead of the more traditional f .x1 ; : : : ; xn /. However, for this monograph, we will use the more traditional syntax. We will also write some binary functions in the traditional infix form, thus writing x C y instead of C.x; y/. The constants in ACL2 comprise what is known as the ACL2 universe. The universe is open but contains numbers, characters, strings, certain types of constant symbols, and ordered pairs. We quickly recount their representations below: Numbers are represented as in traditional mathematics, for example, 2, 1, 22=7,
etc. The universe contains rational and complex rational numbers. Characters are represented in a slightly unconventional syntax, for example, the
character a is represented by #\a. We will not use characters in this monograph. A string
Data Loading...
