Computer-Aided Reasoning: An Approach

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

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:

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.

Errata

All the errors noted below have been corrected in the paperback version of the book distributed via lulu (see Ordering Information). However, if you have the Kluwer hardback version or a non-most-recent paperback version, the notes below may be helpful.

To accommodate readers of all past versions, we locate the known errors in two ways.

First, we generally give the section, paragraph, and sentence number of the sentence containing the error. In the manuscript, the first paragraph of every section is not indented; all other paragraphs are indented. We count paragraphs from 1. Text following a display (e.g., a formula or itemization) is not counted as a new paragraph unless it is indented. Sentences end with a period and are counted from 1.

The second error locator is the page number in the Kluwer hardback edition followed by the line number. Generally, each page of the Kluwer edition begins with a header containing the page number, the book or chapter title, and a horizontal line spanning the page. We count all non-blank lines below the horizontal line (i.e., we do not count the header itself and we do count all subsequent non-blank lines, whether they are part of a section title, display, or ordinary text). The hardback page and line numbers may not exactly correspond to those in the paperback versions.