[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: Azerbaijanian; Estonian; Polish; Spanish; Swedish; Turkish.]
The book is meant for two audiences: those looking for innovative ways to design, build, and maintain hardware and software systems faster and more reliably, and those wishing to learn how to do this. The former audience includes project managers and students in survey-oriented courses. The latter audience includes students and professionals pursuing rigorous approaches to hardware and software engineering or formal methods. The book can be used in graduate and upper-division undergraduate courses on Software Engineering, Formal Methods, Hardware Design, Theory of Computation, Artificial Intelligence, and Automated Reasoning.
The book is divided into two parts. Part I begins with a discussion of the effort involved in using ACL2. It also contains a brief introduction to the ACL2 logic and its mechanization, which is intended to give the reader sufficient background to read the case studies. A more thorough, textbook introduction to ACL2 may be found in the companion book, Computer-Aided Reasoning: An Approach.
ACL2 is an improved and extended version of the ``Boyer-Moore theorem prover,'' Nqthm, adapted to applicative Common Lisp. Editors Kaufmann and Moore are the authors of the ACL2 system. (Bob Boyer also made substantial early contributions to ACL2.) ACL2 may be obtained for free under the terms of GNU General Public License from the ACL2 home page, which includes not only source code and extensive hypertext documentation but also many papers about ACL2 and its applications, guided tours of the system, and mailing lists.
The heart of the book is Part II, where the case studies are presented. The case studies cover a broad range of applications, from hardware (e.g., floating-point arithmetic, hardware description languages, and symbolic trajectory analysis) to software (e.g., graph searching, compiling, and a model checking algorithm) and beyond (number theory and real analysis). All are done in a single, mechanically supported mathematical framework: ACL2.
The full solution to each case study is available here. For example, when we say that one of the case studies formalizes a floating-point multiplier and proves it correct, we mean that not only can you read an English description of the model and how it was proved correct, but you can obtain the entire formal content of the project and replay the proofs, if you wish, with your copy of ACL2. Thus, this book is just the beginning. If you really want to learn how to prove a floating-point multiplier or compiler correct, read the articles and then get the scripts and reproduce the proofs. Then modify them and experiment.
The case studies contain exercises whose solutions are on the Web. In addition, the complete ACL2 scripts necessary to formalize the models and prove all the properties discussed are on the Web. If you want to master the techniques used to do a particular project, do the exercises in the case studies that look similar to your project.
| Piergiorgio Bertoli |
IRST - Istituto per la Ricerca Scientifica e Tecnologica Povo, Italy |
| Dominique Borrione |
TIMA-UJF Grenoble, France |
| John Cowles |
Department of Computer Science University of Wyoming Laramie, Wyoming |
| Arthur Flatau |
Advanced Micro Devices, Inc. Austin, Texas |
| Ruben Gamboa |
Logical Information Machines, Inc. Austin, Texas |
| Philippe Georgelin |
TIMA-UJF Grenoble, France |
| Wolfgang Goerigk |
Institut fur Informatik und Praktische Mathematik Christian-Albrechts-Universitat zu Kiel Kiel, Germany |
| David Greve |
Rockwell Collins Advanced Technology Center Cedar Rapids, Iowa |
| David Hardin |
Ajile Systems, Inc. Oakdale, Iowa |
| Warren A. Hunt, Jr. |
IBM Austin Research Laboratory Austin, Texas |
| Damir A. Jamsek |
IBM Austin Research Laboratory Austin, Texas |
| Matt Kaufmann |
Advanced Micro Devices, Inc. Austin, Texas |
| Panagiotis Manolios |
Department of Computer Sciences University of Texas at Austin Austin, Texas |
| William McCune |
Mathematics and Computer Science Division Argonne National Laboratory Argonne, Illinois |
| J Strother Moore |
Department of Computer Sciences University of Texas at Austin Austin, Texas |
| Vanderlei Rodrigues |
TIMA-UJF Grenoble, France (on leave from UFRGS, Porto Alegre, Brazil) |
| David M. Russinoff |
Advanced Micro Devices, Inc. Austin, Texas |
| Jun Sawada |
Department of Computer Sciences, University of Texas at Austin Austin, Texas |
| Olga Shumsky |
Department of Electrical and Computer Engineering Northwestern University Evanston, Illinois |
| Paolo Traverso |
IRST - Istituto per la Ricerca Scientifica e Tecnologica Povo, Italy |
| Matthew Wilding |
Rockwell Collins Advanced Technology Center Cedar Rapids, Iowa |
The authors of the case studies have supplied full scripts to reproduce the
results presented. This ``supporting material'' also contains the solutions
to the exercises in each case study. There is a separate directory for each
case study's supporting material, to be found under the
workshops/1999 directory, which you
can download
from GitHub. There is a top-level README file, and
each subdirectory contains a README file that explains
its contents.
5. An Exercise in Graph Theory
(J Moore; directory graph/)
The chapter formalizes and proves the correctness of several
simple algorithms for determining whether a path exists between two nodes of
a finite directed graph.
6. Modular Proof: The Fundamental Theorem of Calculus
(Matt Kaufmann; directory calculus/)
The chapter presents a modular top-down proof methodology and
uses it to formalize and prove the Fundamental Theorem of Calculus. The
modular strategy works for both ACL2 and ``ACL2(r)'' (see Chapter 18 below); the
Fundamental Theorem is proved with ACL2(r).
7. Mu-Calculus Model-Checking
(Panagiotis Manolios; directory mu-calculus/)
The chapter presents a formal development of the syntax and
semantics for the Mu-calculus, a model-checker for it in ACL2, and a
discussion of the translation of other temporal logics into the Mu-calculus.
The model checker is proved correct.
8. High-Speed, Analyzable Simulators
(David Greve, Matthew Wilding, David Hardin;
directory simulator/)
High-speed simulation models are routinely developed during the
design of complex hardware systems in order to predict performance, detect
design flaws, and allow hardware/software co-design. Writing such an
executable model in ACL2 brings the additional benefit of formal analysis;
however, much care is required to construct an ACL2 model that is both fast
and analyzable. In this chapter, techniques are described for the
construction of high-speed formally analyzable simulators in ACL2. Their
utility is demonstrated on a simple processor model.
9. Verification of a Simple Pipelined Machine Model
(Jun Sawada; directory pipeline/)
An ACL2 model of a three-stage pipelined machine is defined,
along with a model of the corresponding sequential machine. Then a proof of
the equivalence between the two machines is presented. More importantly, the
method of decomposing the proof applies to much more complicated pipelined
architectures.
10. The DE Language
(Warren Hunt, Jr.; directory de-hdl/)
The DE language is an occurrence-oriented description language
that permits the hierarchical definition of finite-state machines in the
style of a hardware description language. The syntax and semantics of the
language are formalized and the formalization is used to prove the
correctness of a simple hardware circuit. Such formal HDLs have been used to
prove properties of much more complicated designs.
11. Using Macros to Mimic VHDL
(Dominique Borrione, Philippe Georgelin, Vanderlei Rodrigues;
directory vhdl/)
The purpose of this project was to formalize a small
synthesizable behavioral subset of VHDL, preserving as much as possible the
syntactic flavor of VHDL and facilitating verification by symbolic simulation
and theorem proving.
12. Symbolic Trajectory Evaluation
(Damir A. Jamsek; directory ste/)
Symbolic Trajectory Evaluation (STE) is a form of model checking
fundamentally based on symbolic simulation. This chapter presents a formal
treatment of STE, including ACL2 proofs of results presented in the Seger and
Joyce paper ``A Mathematically Precise Two-Level Formal Hardware Verification
Methodology.''
13. RTL Verification: A Floating-Point Multiplier
(David M. Russinoff, Arthur Flatau;
directory multiplier/)
This chapter describes a mechanical proof system for designs
represented in the RTL language of Advanced Micro Devices. The system
consists of a translator to ACL2 and a methodology for verifying properties
of the resulting programs using the ACL2 prover. The correctness of a simple
floating-point multiplier is proved.
14. Design Verification of a Safety-Critical Embedded Verifier
(Piergiorgio Bertoli, Paolo Traverso;
directory embedded/)
This chapter shows the use of ACL2 for the design verification of
a piece of safety-critical software, the Embedded Verifier. The Embedded
Verifier checks online that each execution of a safety-critical translator is
correct. The translator is a component of a software system used by Union
Switch and Signal to build trainborne control systems.
15. Compiler Verification Revisited
(Wolfgang Goerigk; directory compiler/)
This study illustrates a fact observed by Ken Thompson in his
Turing Award Lecture: the machine code of a correct compiler can be altered
to contain a Trojan Horse so that the compiler passes almost every test,
including the so-called ``bootstrap test'' in which it compiles its own
source code with identical results, and still be capable of generating
``bad'' code. The compiler, the object code machine, and the experiments are
formalized in ACL2.
16. Ivy: A Preprocessor and Proof Checker for First-Order Logic
(William McCune, Olga Shumsky; directory ivy/)
In this case study, a proof checker for first-order logic is
proved sound for finite interpretations. In addition, the study shows how
non-ACL2 programs can be combined with ACL2 functions in such a way that
useful properties can be proved about the composite programs. Nothing is
proved about the non-ACL2 programs. Instead, the results of the non-ACL2
programs are checked at run time by ACL2 functions, and properties of these
checker functions are proved.
17. Knuth's Generalization of McCarthy's 91 Function
(John Cowles; directory knuth-91/)
This chapter deals with a challenge by Donald Knuth for a ``proof
by computer'' of a theorem about his generalization of John McCarthy's famous
``91 function.'' The generalization involves real numbers, and the case
study uses ACL2 to meet Knuth's challenge by mechanically verifying results
not only about the field of all real numbers, but also about every subfield
of that field.
18. Continuity and Differentiability
(Ruben Gamboa; directory analysis/)
This chapter shows how an extended version of ACL2 (named
ACL2(r)) and described can be used to reason about the real and
complex numbers, using non-standard analysis. It describes some
modifications to ACL2 that introduce the irrational real and complex numbers
into ACL2's number system. It then shows how the modified ACL2 can prove
classic theorems of analysis, such as the intermediate-value and mean-value
theorems.