Books and Papers about ACL2 and Its Applications


NOTES:
  1. This list is generally incomplete, and many entries are out-of-date. To search for publications about some ACL2 topic we recommend a standard web search (e.g., Google) and that you include in your search pattern the name ACL2.
  2. See also the ACL2 workshops page for proceedings of ACL2 workshops, which contain numerous papers, many of them recent, that are not found below.
  3. Please feel free to send us email that specifies additions to make to the list below.

This document is divided into the following sections.

About ACL2: Quick Summary of What Can Be Done and How to Learn ACL2

This link will take you to a page on which you can find:

Books

Books about ACL2 and Its Applications

Using the techniques described in these two books, users of the ACL2 system have modeled and proved properties of hardware designs, microprocessors, microcode programs, and software. In addition, many theorems in mathematics and meta-mathematics have been proved with ACL2.

Details:

Book about logic in computing using ACL2

Essential Logic for Computer Science, Rex Page and Ruben Gamboa. ISBN 978-0262039185. MIT Press, 2019.

This book is an introduction to the use of predicate logic and ACL2 for testing and verifying software and digital circuits. It has been used as a textbook in an honors introductory course in computing, and with supplementary materials in a course in discrete mathematics.

Book about a predecessor of ACL2

A Computational Logic, R. S. Boyer and J S. Moore. Academic Press, New York, 1979. xiv+397. The original Pub source for the book is here. The translation to TeX and pdf was kindly done by Gary Klimowicz. The above book is out of print. The copyright has reverted to the authors.

We hereby place it in the public domain.

Book about customized reasoning tools

Scalable Techniques for Formal Verification, Sandip Ray. ISBN 978-4419-5997-3. Springer, 2010.

This book explains how to develop customized reasoning tools on top of ACL2. The customized reasoning tools extend ACL2 by significantly automating formal proofs on their target domains, but without requiring any modification to the theorem prover source code.

Book about high-assurance microprocessors

Design and Verification of Microprocessor Systems for High-Assurance Applications, David S. Hardin, ed. Springer, 2010. Quoting from the abstract:
This book examines several leading-edge design and verification technologies that have been successfully applied to microprocessor systems for high-assurance applications at various levels -- from arithmetic circuits to microcode to instruction sets to operating systems to applications. We focus on recent hardware, software, and system designs that have actually been built and deployed, and feature systems that have been certified at high Evaluation Assurance Levels, namely the Rockwell Collins AAMP7G microprocessor (EAL7) and the Green Hills INTEGRITY-178B separation kernel (EAL6+). The contributing authors to this book have endeavored to bring forth truly new material on significant, modern design and verification efforts; many of the results described herein were obtained only within the past year.
Several chapters in this book describe ACL2 proof developments.

Book about formal floating-point hardware verification

Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, David M. Russinoff. Springer, 2019. In the author's words:

This is the first book to focus on the problem of ensuring the correctness of floating-point hardware designs through mathematical methods. It advances a verification methodology based on a unified theory of register-transfer logic and floating-point arithmetic that has been developed and applied to the formal verification of commercial floating-point units over the course of more than two decades, during which the author was employed by several major microprocessor design companies. The entire theory and all applications reported have been formalized and mechanically verified with ACL2.

Papers

The best introduction to ACL2 is the first of the two books above. But if you prefer to read papers on the Web, we recommend the first two papers in Overviews.

Typical formalization problems raise many issues that are not yet adequately addressed in ACL2 (or any other mechanized formal system). If you are trying to formalize a problem in ACL2, you may well have to formalize some ideas for the first time, while extending the work of others. It is often helpful to separate the issues involved in your problem and to try to find papers below that seem likely to touch upon some of those same issues. Then look at those papers for ideas about how to deal with your problems. A comprehensive set of case studies is presented in the second of the two books above.

Several of the papers listed contain links to ACL2 scripts.

If you have a paper (preferably in postscript format) or a URL related to an ACL2 application or extension and would like it linked into this page, please contact moore@cs.utexas.edu.

Overviews

Foundations

ACL2 Capabilities

Utilities

Data Structures

Processor Modeling and Hardware Verification

See also the previously mentioned book, "Design and Verification of Microprocessor Systems for High-Assurance Applications", for a variety of papers by various authors on processing modeling in ACL2 (and other systems).

Programming Languages and Software Verification

Floating Point Arithmetic

Real Arithmetic

Concurrency

Model Checking and Symbolic Trajectory Evaluation

Logic and Metamathematics

Miscellaneous Applications

Related Web Sites