- Description
- Table of Contents and Excerpts (pdf .2Mb) (ps .8Mb).
- Appendices ("Using the ACL2 System", "Additional Features"), Bibliography, and Index (pdf)
- Errata
- Solutions to Exercises
- Ordering Information

[For some foreign translations of (possibly earlier) versions of this page (not the book!) see the following links. The authors of ACL2 have no control over what you will find at these links: Russian; Belarussian; Latvian; Ukranian.]

Current hardware and software systems are often very complex and the trend is towards increased complexity. By modeling systems mathematically, we obtain models that we can prove behave correctly. To further increase confidence in our reasoning, which may be complex, we can use a computer program to check our proofs and even to automate some of their construction.

In this book we present:

- A practical functional programming language closely related to Common
Lisp which is used to define functions (which can model computing systems)
and to make assertions about defined functions.
- A formal logic in which defined functions correspond to axioms; the logic is
first-order, includes induction, and allows us to prove theorems about the
functions.
- The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process.

We use a particular formalism and a particular mechanization of it, namely ACL2, which is freely available under the terms of a BSD-style license from the ACL2 home page. ACL2 was written by Kaufmann and Moore and is the successor to the ``Boyer-Moore theorem prover,'' Nqthm. (Bob Boyer also made substantial early contributions to ACL2.) The ACL2 home page includes the online reference manual, which is a large hypertext document meant primarily for users of the system. This book is the definitive introduction to ACL2 and how to use it.

While teaching the use of mechanized formalism, we focus on computational problems of the sort typically faced by someone using formal methods to analyze computer hardware or software.

ACL2 is used in industry. Remember the Intel FDIV bug? The first Pentium [trademark, Intel, Inc] could not divide floating-point numbers correctly and it reportedly cost Intel $500 million to fix. At the time that was happening, we used ACL2 to verify that the floating point division microcode on AMD's competing microprocessor, the AMD-K5, was correct. AMD used ACL2 to verify the elementary floating-point operations for the recently released Athlon. [Note: AMD, the AMD logo and combinations thereof, AMD-K5, AMD-K7, and AMD Athlon are trademarks of Advanced Micro Devices, Inc.] The companion volume presents a closely related case study.

The ACL2 system has been successfully applied to projects of commercial
interest, including microprocessor modeling, hardware verification, microcode
verification, and software verification. This book gives a methodology for
modeling computing systems formally and for reasoning about those models with
mechanized assistance. The practicality of computer-aided reasoning is
further demonstrated in the companion book, *Computer-Aided Reasoning: ACL2 Case Studies*.