Computer-Aided Reasoning: An Approach

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

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; Spanish; Macedonian; Polish; Turkish; French; Azerbaijanian; Marathi; Ukrainian.]

Description

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:

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.

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.