Computer-Aided Reasoning: ACL2 Case Studies

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


This book illustrates how the computer-aided reasoning system ACL2 can be used in productive and innovative ways to design, build, and maintain hardware and software systems. Included here are technical papers written by twenty-one contributors that report on self-contained case studies, some of which are ``sanitized'' industrial projects. They deal with a wide variety of ideas, including floating-point arithmetic, microprocessor simulation, model checking, symbolic trajectory evaluation, compilation, proof checking, real analysis, and several others.

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.


The contributors to this volume are listed below along with their affiliations at the time of the work.
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
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


Supporting Material for the Case Studies, Including Solutions to Exercises

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, if you download the "workshops" books from the ACL2 community books repository. 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.