Computer-Aided Reasoning: An Approach

Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Kluwer Academic Publishers, June, 2000. (ISBN 0-7923-7744-3)

[For a Russian translation of an earlier version of this page (not the book!) see the following link. The authors of ACL2 have no control over what you will find at this link.


This book is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on Software Engineering or Formal Methods. It is also suitable in conjunction with other books in courses on Hardware Design, Discrete Mathematics, or Theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on Artificial Intelligence or Automated Reasoning.

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:

This book will teach you how to formalize things, how to construct proofs, and how to use a mechanical tool to check those proofs.

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.