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
• Books about ACL2 and Its Applications
• Papers about ACL2 and Its Applications, which is subdivided as follows.
• Overviews
• Foundations
• ACL2 Capabilities
• Utilities
• Data Structures
• Processor Modeling and Hardware Verification
• 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

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

• a brief paper about ACL2 and applications;
• exercises, which provide the best way to learn ACL2;
• a paper with lots of tips on how to program and prove theorems with ACL2; and
• additional tutorial material.

Books about ACL2 and Its Applications

• How to use ACL2:
  Computer-Aided Reasoning: An Approach, Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Kluwer Academic Publishers, June, 2000. (ISBN 0-7923-7744-3)

• What can be done with ACL2:
  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)

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:

• Computer-Aided Reasoning: An Approach: description, excerpts, errata, solutions to exercises.
• Computer-Aided Reasoning: ACL2 Case Studies: description, list of contributors, excerpts, errata, full scripts for case studies, solutions to exercises.
• ACL2 Home Page: tours of the system, documentation, technical papers, source code, installation guide, mailing lists.
• Ordering Information
• 1999 ACL2 Wizard's Workshop: this was the meeting that produced the two books above; it was the first in a planned series of workshops for the ACL2 community.

Book about a predecessor of ACL2

We hereby place it in the public domain.

Papers about ACL2 and Its Applications

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

• About ACL2

• ACL2 Theorems about Commercial Microprocessors, Bishop Brock, Matt Kaufmann and J Moore, in M. Srivas and A. Camilleri (eds.) Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, pp. 275-293, 1996. The paper sketches the system and two industrial applications: the AMD5K86 floating-point division proof and the Motorola CAP DSP model.

• An Industrial Strength Theorem Prover for a Logic Based on Common Lisp Matt Kaufmann and J Moore, IEEE Transactions on Software Engineering 23(4), April 1997, pp. 203-213. We discuss how we scaled up the Nqthm (``Boyer-Moore'') logic to Common Lisp, preserving the use of total functions within the logic but achieving Common Lisp execution speeds, via the introduction of ``guards.''

• Hyper-Card for ACL2 Programming by Matt Kaufmann and J Moore. This is a quick reference sheet with lots of hyper-text links to the online documentation. It also contains a gentle introduction to Lisp programming.

• A Computational Logic for Applicative Common Lisp, Matt Kaufmann and J Moore. In: A Companion to Philosophical Logic, D. Jacquette (ed.), Blackwell Publishers, pp. 724-741, 2002.

• Design Goals of ACL2, Matt Kaufmann and J Moore, CLI Technical Report 101, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX 78703, 1994. This is an early report identifying aspects of Nqthm of special concern during the design of ACL2.

• Maintaining the ACL2 Theorem Proving System, Matt Kaufmann and J Strother Moore. Invited talk. Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning (G. Sutcliffe, R. Schmidt, and S. Schulz, eds.), CEUR Worksho Proceedings Vol. 192, Seattle, Washington, August 2006.

• Some Key Research Problems in Automated Theorem Proving for Hardware and Software Verification, Matt Kaufmann and J Strother Moore. Revista de la Real Academia de Ciencias (RACSAM), Vol. 98, No. 1, pp. 181--196, 2004. Spanish Royal Academy of Science.

• ACL2 Support for Verification Projects, Matt Kaufmann. Invited talk, Proc. 15th Intl. Conf. on Automated Deduction, ed. C. Kirchner and H. Kirchner, Lec. Notes Artif. Intelligence 1421, Springer-Verlag, Berlin, 1998, pp. 220--238.

• An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, Matt Kaufmann and J Moore). IEEE Transactions on Software Engineering 23}, no. 4, April 1997, 203--213.

• Design Goals for ACL2, Matt Kaufmann and J Strother Moore. In proceedings of: Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Kiel, Germany (1994), pp. 92-117. Published by Christian-Albrechts-Universitat.

Foundations

• Integrating External Deduction Tools with ACL2, Matt Kaufmann, J S. Moore, Sandip Ray, and Erik Reeber. Journal of Applied Logic (Special Issue: Empirically Successful Computerized Reasoning), Volume 7, Issue 1, March 2009, pp. 3--25. Published online, DOI 10.1016/j.jal.2007.07.002. Preliminary version in C. BenzmŸller, B. Fischer, and G. Sutcliffe (eds.), Proceedings of the 6th International Workshop on the Implementation of Logics (IWIL 2006), Phnom Penh, Cambodia, November 2006, pages 7-26. Volume 212 of CEUR Workshop Proceedings.

• An Integration of HOL and ACL2, Michael J.C. Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD'06) (A. Gupta and P. Manolios, eds.). IEEE Computer Society Press, pp. 153-160, November, 2006. Slides are available here.
  See also: An Embedding of the ACL2 Logic in HOL, Michael J.C. Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds. In P. Manolios and M. Wilding (eds.), Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, pages 40-46. To Appear in ACM Digital Library. ©ACL2 Steering Committee.

• Integrating CCG analysis into ACL2, Matt Kaufmann, Panagiotis Manolios, J Moore, and Daron Vroon). Proceedings of The Eighth International Workshop on Termination (WST 2006), August, 2006.

• Quantification in Tail-recursive Function Definitions, Sandip Ray. In P. Manolios and M. Wilding (eds.), Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, pages 95-98. To Appear in ACM Digital Library. ©ACL2 Steering Committee.

• Adding a Total Order to ACL2, M. Kaufmann and P. Manolios. In Proceedings of ACL2 Workshop 2002.

• Single-Threaded Objects in ACL2, Robert Boyer and J Moore. Single-threaded objects in ACL2 are structures that have the normal ``copy-on-write'' applicative semantics one expects in a functional programming language but which are implemented by destructive modification. The axiomatic ``story'' is consistent with the implementation because syntactic restrictions are enforced which insure that only the modified structure is subsequently referenced. Single-threaded objects (or ``stobjs'') are particularly useful in modeling microprocessors, where the state of the processor is modeled as a stobj.

• Structured Theory Development for a Mechanized Logic, M. Kaufmann and J Moore, Journal of Automated Reasoning 26, no. 2 (2001), pp. 161-203. This paper presents a precise development of the encapsulate and include-book features of ACL2 and gives careful proofs of the high-level correctness properties of these ACL2 structuring mechanisms.

• A Precise Description of the ACL2 Logic, Matt Kaufmann and J Moore, April, 1998. This paper is a working draft of a precise description of the base logic. The draft does not describe the theorem prover or the system; it is a dry mathematical document describing the logic from first principles. At the moment the description omits encapsulation, multiple values, property lists, arrays, state, and macros.

• The ACL2 User's Manual, Matt Kaufmann and J Moore. The user's manual is a hypertext document. It is most useful in its HTML or Texinfo forms. However, we have created a gzipped Postscript version (1.5 MB). It is roughly 1300 pages long and includes, near the end, a Table of Contents and an Index.

ACL2 Capabilities

• Efficient execution in an automated reasoning environment, David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, Jose' Luis Ruiz-Reina, Rob Sumners, Daron Vroon and Matthew Wilding. Journal of Functional Programming, Volume 18, Issue 01, January 2008. Cambridge University Press.

• Double Rewriting for Equivalential Reasoning in ACL2, Matt Kaufmann and J Strother Moore. In P. Manolios and M. Wilding (eds.), Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, pages 103-106. To Appear in ACM Digital Library. ©ACL2 Steering Committee.

• Linear and Nonlinear Arithmetic in ACL2, Warren A. Hunt Jr., Robert Bellarmine Krug, and J Moore. In CHARME 2003, D. Geist (ed.), Springer Verlag LNCS 2860, pp. 319-333, 2003. This paper describes the mechanization of linear and nonlinear arithmetic in ACL2.

• Integrating Nonlinear Arithmetic into ACL2, Warren A. Hunt Jr., Robert Bellarmine Krug, and J Moore. In Proceedings of ACL2 Workshop 2004. This paper presents an overview of the integration of a nonlinear arithmetic reasoning package into ACL2.

• Meta Reasoning in ACL2, Warren A. Hunt Jr, Matt Kaufmann, Robert Bellarmine Krug, J Moore, and Eric W. Smith. In 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer Lecture Notes in Computer Science, 3603, pp. 163--178, 2005. This paper describes the variety of meta-reasoning facilities in ACL2.

Utilities

• Attaching Efficient Executability to Partial Functions in ACL2, Sandip Ray. In M. Kaufmann and J S. Moore (eds.), 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004.

• A Tool for Simplifying Files of ACL2 Definitions, Matt Kaufmann. In Proceedings of ACL2 Workshop 2003. If you obtain the workshops books, see books/workshops/2003/kaufmann/.

• ACL2 Interaction via Emacs, Bishop Brock, 1998. This is a collection of Emacs programs to speed up interaction between ACL2 and Emacs. If you typically interact with ACL2 via an Emacs buffer, you may be surprised to know that up to half of the time you spend waiting for an ACL2 command to complete is due to Emacs display overhead. This package includes freely distributable source code for two effective approaches to reducing this overhead. The first approach is very general and provides pretty good results. The other approach is a bit of a hack, but practically eliminates display overhead for long ACL2 runs. To try these out, download the following file. You should name the file acl2-emacs.tar.gz. After downloading it, decompress and untar it with

  % tar -xvzf acl2-emacs.tar.gz

  and read the enclosed note in report.ps. Here is the file to download, but don't click on it as you would a normal link or you may get a browser screen of gibberish. Click on it to download (e.g., in Netscape, Shift+Button 1 (hold shift and click the left mouse button) or Button 3 and then select ``Save link as...''). acl2-emacs.tar.gz

• Infix Printing, Mike Smith, 1998.

  An infix syntax for ACL2 has been implemented by Mike Smith. Two capabilities are supported.

  • IACL2 is an infix version of the ACL2 theorem proving system that performs I/O in infix format. It is intended to make initial experiments with ACL2 somewhat simpler for those unfamiliar with or opposed to Lisp prefix syntax. (It is not an interface for experts, as some of the more advanced aspects of ACL2 are not supported by the infix parser.) Some examples of the syntax:

        Function idiv (m : integer, n : integer | n ~~= 0)
         { ifix ( m/n ) };
    
        /* Idiv takes two integer arguments, the second of which cannot = zero */
    
        Theorem distributivity-of-minus-over-plus
         {-(x + y) = -x + -y};
    
        Theorem car-nth-0 { consp(x) -> x.car = x[0] };
    

  • We provide formatting support to help the user publish ACL2 event files. The syntax produced is either standard ACL2 or ``conventional'' infix mathematical notation with formatted comments and doc-strings. For example, in LaTeX mode comments are formatted as running text, events are indexed and substitutions are made of LaTeX mathematical symbols for various functions. In HTML mode, cross references are created from function usage to definition. Other ouput modes include Scribe and ASCII text. The formatting conventions are user extensible.

  For more information, see the README overview.

Data Structures

• Finite set theory based on fully ordered lists, by Jared Davis, describes the set theory implementation in books/finite-set-theory/osets/. In this library, set equality is just ACL2's "equal" and the typical set operations (union, intersection, difference, cardinality) are linear-time and efficiently implemented. A fairly complete set of set operations and rewrite rules are provided, and "pick a point" proofs can be used to show subset relations. Macros allow the quick introduction of functions to quantify predicates over sets (e.g., "all-less-than"), and map functions over sets (e.g., "cons-onto-each"). More information and slides are also available at the above page.

• Finite Set Theory in ACL2, by J Strother Moore, describes some of the features available in the book books/finite-set-theory/set-theory.lisp distributed with ACL2 (Versions 2.5 and higher). The book provides hereditarily finite sets built from ACL2 objects. Sets are represented by lists. Sets may contain sets as elements. The usual primitives -- including those for dealing with functions as sets of ordered pairs -- are defined and lemmas are proved providing many algebraic properties of finite set theory. Some common proof strategies are codified and macros are provided for defining functions that construct certain sets from others. This book is just a start at what could easily turn into a major effort to support finite set theory more completely.

• Efficient Rewriting of Data Structures in ACL2, M. Kaufmann and R. Sumners. In Proceedings of ACL2 Workshop 2002 This paper describes the so-called "records books", distributed in books/misc/records.lisp and books/misc/records0.lisp.

• An Exercise in Graph Theory, J Moore, Chapter 5 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) The article formalizes and proves the correctness of several simple algorithms for determining whether a path exists between two nodes of a finite directed graph. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Defthms About Zip and Tie: Reasoning About Powerlists in ACL2, Ruben Gamboa, University of Texas Computer Sciences Technical Report No. TR97-02, February, 1998. This work is based on Jay Misra's ``powerlist'' device, a data structure well-suited to recursive, data-parallel algorithms. A generalization of powerlists is formalized in ACL2 by Gamboa and used to prove a variety of algorithm correct, including several sorting algorithms (including bitonic and Batcher), a grey-code sequence generator, and a carry-lookahead adder. ACL2 event lists are linked to the URL above.

• Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2, Ruben Gamboa, in Third International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA), 1998. This paper is based on Jay Misra's work on ``powerlists'' (above) and formalizes Misra's stunningly simple proof of the correctness of an FFT algorithm implemented with powerlists. The URL above links to an ACL2 event script as well.

• Defstructure for ACL2, Bishop Brock, December, 1997. This paper serves as documentation for the ACL2 defstructure book, which provides a ``record facility'' similar to Common Lisp's defstruct and Nqthm's add-shell.

Processor Modeling and Hardware Verification

• Connecting Pre-silicon and Post-silicon Verification. S. Ray and W. A. Hunt, Jr. In A. Biere and C. Pixley, editors, Proceedings of the 9th International Conference on Formal Methods in Computer-aided Design (FMCAD 2009), Austin, TX, November 2009, pages 160-163. IEEE Computer Society.

• Formal Verification for High-Assurance Behavioral Synthesis. S. Ray, K. Hao, Y. Chen, F. Xie, and J. Yang. In Z. Liu and A. P. Ravn, editors, Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA 2009), Macao SAR, China, October 2009, volume 5799 of LNCS, pages 337-351. Springer.

• Abstracting and Verifying Flash Memories, Sandip Ray and Jayanta Bhadra. In K. Campbell, editor, Proceedings of the 9th Non-Volatile Memory Technology Symposium (NVMTS 2008), Pacific Grove, CA, November 2008, pages 100-104. IEEE.

• A Mechanized Refinement Framework for Analysis of Custom Memories, Sandip Ray and Jayanta Bhadra. In J. Baumgartner and M. Sheeran, editors, Proceedings of the 7th International Conference on Formal Methods in Computer-aided Design (FMCAD 2007), Austin, TX, November 2007, pages 239-242. IEEE Computer Society.

• Mechanized Certification of Secure Hardware Designs, Sandip Ray and Warren A. Hunt, Jr. In J. Bhadra, L. Wang, and M. S. Abadir, editors, Proceedings of the 8th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (MTV 2007), Austin, TX, December 2007. IEEE Computer Society.

• Formal Verification of Floating-Point RTL at AMD using the ACL2 Theorem Prover, David Russinoff, Matt Kaufmann, Eric Smith, Robert Sumners. 17th IMACS World Congress: Scientific Computation, Applied Mathematics and Simulation. July, 2005.

• Deductive Verification of Pipelined Machines Using First-order Quantification, Sandip Ray and Warren A. Hunt Jr. In R. Alur and D. A. Peled, editors, Proceedings of the 16th International Conference on Computer-aided Verification (CAV 2004), Boston, MA, July 2004, volume 3117 of LNCS, pages 31-43. ©Springer-Verlag.

• Formal Verification of Microprocessors at AMD, Arthur Flatau, Matt Kaufmann, David F. Reed, David Russinoff, Eric Smith, and Rob Sumners. Proceedings of Designing Correct Circuits 2002.

• High-Speed, Analyzable Simulators, David Greve, Matthew Wilding, and David Hardin, Chapter 8 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) 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 article, techniques are described for the construction of high-speed formally analyzable simulators in ACL2. Their utility is demonstrated on a simple processor model. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Verification of a Simple Pipelined Machine Model, Jun Sawada, Chapter 9 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Verification of Pipeline Circuits, Matt Kaufmann and David M. Russinoff, in Proceedings of ACL2 Workshop 2000.

• The DE Language, Warren Hunt, Jr., Chapter 10 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Using Macros to Mimic VHDL, Dominique Borrione, Philippe Georgelin, and Vanderlei Rodrigues, Chapter 11 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Efficent Simulation of Formal Processor Models, Dave Hardin, Matt Wilding, and Dave Greve, Rockwell Collins, Inc., Advanced Technology Center, Cedar Rapids, IA, May, 1998. This paper describes some ``hacks'' by which ACL2 array processing can be sped up to C speeds. A simple processor model, comparable to the traditional ``small machine'' mentioned above, is used as the benchmark. Native ACL2 achieves simulation speeds of about 19,000 ``small machine'' instructions per second when executing this model. After modifying ACL2 as described, the model is executed at slightly over 2 million instructions per second, comparable to a C model of the processor. Technically, the techniques used in this paper render ACL2 unsound because they assume (without the necessary syntactic checking) that ACL2 arrays are used in a single-threaded way. However, the experiments done in this paper and the techniques used are extremely illuminating. They also indicate modifications that could be made to ACL2 to provide the efficiency needed in industrial-scale modeling, while preserving soundness. The paper is highly recommended.

• Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle, Dave Hardin, Matt Wilding and Dave Greve, in A. J. Hu and M. Y. Vardi (eds.) Computer Aided Verification: 10th International Conference, CAV '98, Springer-Verlag LNCS 1427, 1998. The paper suggests ways to integrate theorem proving into the microprocessor design cycle. The paper was presented at CAV '98. During the talk, the authors demonstrated an ACL2 model of the ALU of the JEM1 (a silicon Java Virtual Machine) microprocessor, its transparent use to compute ALU results for a C-based simulation tool for the processor and ACL2 proofs about the ALU. This demonstration is not discussed in the paper but is indicative of the ideas in the paper.

• Symbolic Simulation: An ACL2 Approach, J Moore, in G. Gopalakrishnan and P. Windley (eds.) Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design (FMCAD'98), Springer-Verlag LNCS 1522, pp. 334-350, November, 1998. ( ACL2 Script) This paper advocates the idea of symbolic simulation of processor models, as a step from the familiar (namely, traditional simulation of C models of designs) to the unfamiliar (namely, proofs about formal models). The papers demonstrates how ACL2 can provide a symbolic simulation capability for the ``small machine'' model. Some interesting performance measures are also given.

Programming Languages and Software Verification

• Mechanized Information Flow Analysis through Inductive Assertions, Warren A. Hunt, Jr., Robert Bellarmine Krug, Sandip Ray, and William D. Young. In A. Cimatti and R. B. Jones, editors, Proceedings of the 8th International Conference on Formal Methods in Computer-aided Design (FMCAD 2008), Portland, OR, November 2008, pages 227-230. IEEE Computer Society.

• Evaluating SFI for a CISC Architecture by Stephen McCamant and Greg Morrisett. In 15th USENIX Security Symposium, (Vancouver, BC, Canada), August 2-4, 2006, pp. 209-224. See also the project page.

• Mechanized Operational Semantics by J Moore (lectures given at Marktoberdorf Summer School 2008). These lectures explain how to formalize an ``operational'' or ``state-transition'' semantics of a von Neumann programming language in a functional programming language. These lectures illustrate the techniques by formalizing a simple programming language called ``M1,'' for ``Machine (or Model) 1.'' It is loosely based on the Java Virtual Machine but has been simplified for pedagogical purposes. They demonstrate the executability of M1 models. Several styles of code proofs are developed, including direct (symbolic simulation) proofs based on Boyer-Moore ``clock functions'' and Floyd-Hoare inductive assertion proofs. Proofs are constructed only for the simplest of programs, namely an iterative factorial example. But to illustrate a more realistic use of the model, the correctness proof for an M1 implementation of the Boyer-Moore fast string searching algorithm is discussed.

• A Mechanical Analysis of Program Verification Strategies, Sandip Ray, Warren A. Hunt, Jr. John Matthews, and J Strother Moore. Journal of Automated Reasoning. volume 40(4), May 2008, pages 245-269. Springer.

• Verification Condition Generation via Theorem Proving, John Matthews, J S. Moore, Sandip Ray, and Daron Vroon. In M. Hermann and A. Voronkov, editors, Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Phnom Penh, Cambodia, November 2006, volume 4246 of LNCS, pages 362-376. ©Springer-Verlag

• A Verifying Core for a Cryptographic Language Compiler, Lee Pike, Mark Shields, and John Matthews. In P. Manolios and M. Wilding (eds.), Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, pages 95-98. To Appear in ACM Digital Library. ©ACL2 Steering Committee. See also the supporting materials.

• Proof Styles in Operational Semantics, Sandip Ray and J S. Moore. In A. J. Hu and A. K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-aided Design (FMCAD 2004), Austin, TX, November 2004, volume 3312 of LNCS, pages 67-81. ©Springer-Verlag.

• Design Verification of a Safety-Critical Embedded Verifier, Piergiorgio Bertoli and Paolo Traverso, Chapter 14 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) This article 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Compiler Verification Revisited, Wolfgang Goerigk, Chapter 15 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Proving Theorems about Java-like Byte Code, J Moore, in E.-R. Olderog and B. Steffen (eds.) Correct System Design -- Issues, Methods and Perspectives, LNCS (to appear, 1999). This paper describes a formalization of an abstract machine very similar to the Java Virtual Machine but far simpler. Techniques are developed for specifying the properties of classes and methods for this machine. The paper illustrates two such proofs, that of a static method implementing the factorial function and of an instance method that destructively manipulates objects in a way that takes advantage of inheritance. An ACL2 Script is also available.

• Mechanized Formal Reasoning about Programs and Computing Machines, Bob Boyer and J Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996. This paper explains a formalization style that has been extremely successful in enabling mechanized reasoning about programs and machines, illustrated in ACL2. This paper presents the so-called ``small machine'' model, an extremely simple processor whose state consists of the program counter, a RAM, an execute-only program space, a control stack and a flag. The paper explains how to prove theorems about such models. Accompanying the paper is an ACL2 Script: After fetching this script, use include-book to load it into your ACL2 and then do (in-package "SMALL-MACHINE").

Floating Point Arithmetic

• A Formal Theory of Register-Transfer Logic and Floating-Point Arithmetic, David Russinoff. This is a user's manual for an ACL2 library of floating-point arithmetic as well as an exposition of the underlying theory.

• A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon Processor, David Russinoff. Invited paper in Warren A. Hunt Jr. and Steven D. Johnson (eds.), Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (FMCAD 2000), Springer-Verlag LNCS 1954, 2000. This is a proof of IEEE-compliance, as an application of a mechanical proof system for RTL designs based on ACL2.

• RTL Verification: A Floating-Point Multiplier, David M. Russinoff and Arthur Flatau, Chapter 13 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) This article 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm, J Moore, Tom Lynch, and Matt Kaufmann, IEEE Transactions on Computers, 47(9), pp. 913-926, Sep., 1998. This is the original ( March, 1996) version of our paper describing the mathematical details of the proof that the FDIV microcode on the AMD K5 correctly implements IEEE floating point division. The paper underwent extensive revision during the reviewing process.

• A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD K7 Floating Point Multiplication, Division and Square Root Instructions, David Russinoff, Advanced Micro Devices, Inc., January, 1998. This paper is a tour de force in mechanical verification. The paper describes a mechanically verified proof of correctness of the floating-point multiplication, division, and square root instructions of The AMD K7 microprocessor. The instructions, which are based on Goldschmidt's Algorithm, are implemented in hardware and represented by register-transfer level specifications, the primitives of which are logical operations on bit vectors. On the other hand, the statements of correctness, derived from IEEE Standard 754, are arithmetic in nature and considerably more abstract. Therefore, the paper develops a theory of bit vectors and their role in floating-point representations and rounding, extending previous work (below) in connection with the K5 FPU. The paper then presents the hardware model and a rigorous and detailed proof of its correctness. All of the definitions, lemmas, and theorems have been formally encoded in the ACL2 logic, and every step in the proof has been mechanically checked with the ACL2 prover.

• A Mechanically Checked Proof of IEEE Compliance of the AMD K5 Floating-Point Square Root Microcode, David Russinoff, Formal Methods in System Design Special Issue on Arithmetic Circuits, 1997. The paper presents a rigorous mathematical proof of the correctness of the FSQRT instruction of the AMD K5 microprocessor. The instruction is represented as a program in a formal language that was designed for this purpose, based on the K5 microcode and the architecture of its FPU. The paper proves a statement of its correctness that corresponds directly with the IEEE standard. It also derives an equivalent formulation, expressed in terms of rational arithmetic, which has been encoded as a formula in the ACL2 logic and mechanically verified with the ACL2 prover. Finally, the paper describes a microcode modification that was implemented as a result of this analysis in order to ensure the correctness of the instruction.

Real Arithmetic

• Non-Standard Analysis in ACL2, Ruben A. Gamboa and Matt Kaufmann, Journal of Automated Reasoning 27(4), 323-351, 2001. This paper describes ACL2(r), a version of ACL2 with support for the real and complex numbers. The modifications are based on non-standard analysis, which interacts better with the discrete flavor of ACL2 than does traditional analysis. See below for a little more about ACL2(r).

• Modular Proof: The Fundamental Theorem of Calculus, Matt Kaufmann, Chapter 6 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) The article 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 above); the Fundamental Theorem is proved with ACL2(r). The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Continuity and Differentiability, Ruben Gamboa, Chapter 18 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) This article shows how an extended version of ACL2 (named ``ACL2(r)'' and described below) 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. The ACL2(r) scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• ACL2 supports the rational numbers but not the reals. Starting with Version 2.5, however, a variant of ACL2 called ``ACL2(r)'' supports the real numbers by way of non-standard analysis. ACL2(r) was produced by Ruben Gamboa from ACL2. ACL2(r) can be built from the ACL2 sources (Versions 2.5 and higher). See the makefile for instructions for building ACL2(r). For further acknowledgements and some technical details see the documentation topic REAL in the online documentation for ACL2. ACL2 authors Kaufmann and Moore consider ACL2(r) Version 2.5 to be in ``beta release.'' They have tried to ensure that when ACL2 is built from the integrated source files, the result is a sound ACL2. They are confident that ACL2(r) will eventually be sound and behave much as it does in the Version 2.5 release, but have not yet checked every detail of the integration. For the foundations of ACL2(r), see Gamboa's Ph.D. dissertation Mechanically Verifying Real-Valued Algorithms in ACL2 (UT, May, 1999). The dissertation includes ACL2(r)-checked proofs of many fundamental properties of the real numbers, including such results as the continuity of e^x, Euler's identity, the basic identities of trigonometry, the intermediate value theorem, and others.

• Square Roots in ACL2: A Study in Sonata Form, Ruben Gamboa, UTCS Tech Report TR96-34, November, 1996. This paper describes a proof in ACL2 that (* x x) is never 2. This was the beginning of Gamboa's journey into the ACL2 mechanization of non-standard analysis.

Concurrency

• A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View, J Moore, February, 1998. This paper presents an ACL2 proof that an n-processor concurrent system implements a non-blocking counter. This paper illustrates one method for dealing with concurrency and nondeterminism in ACL2, by formalizing a compositional semantics for a shared-memory concurrent system. ( ACL2 script).

• An ACL2 Proof of Write Invalidate Cache Coherence, J Moore, in A. J. Hu and M. Y. Vardi (eds.) Computer Aided Verification: 10th International Conference, CAV '98, Springer-Verlag LNCS 1427, pp. 29-38, 1998. This paper presents a pedagogical example of the use of ACL2. An extremely simple cache coherence property is formalized and proved. The intended contribution of the paper is not in the realm of cache coherence -- the problem dealt with here is far too simple for that -- but in demonstrating the ACL2 in a simple modeling project and in one approach to concurrency. (ACL2 Scripts)

• Interactive Consistency in ACL2, Bill Young, Computational Logic, Inc., March, 1997. This paper presents an ACL2 translation of Rushby's PVS improvement to Bevier and Young's Nqthm formalization of the Pease, Shostak and Lamport Oral Messages (``Byzantine Generals'') problem.

Model Checking and Symbolic Trajectory Evaluation

• Combining Theorem Proving with Model Checking through Predicate Abstraction, Sandip Ray and Rob Sumners. IEEE Design & Test of Computers, volume 24(2), March-April 2007 (Special Issue on Advances in Functional Validation through Hybrid Techniques), pages 132-139.

• Reducing Invariant Proofs to Finite Search via Rewriting, Rob Sumners and Sandip Ray. In M. Kaufmann and J S. Moore, editors, 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004.

• Certifying Compositional Model Checking Algorithms in ACL2, Sandip Ray, John Matthews, and Mark Tuttle. In 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003), Boulder, CO, July 2003.

• Mu-Calculus Model-Checking, Panagiotis Manolios, Chapter 7 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) The article 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Symbolic Trajectory Evaluation, Damir A. Jamsek, Chapter 12 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) Symbolic Trajectory Evaluation (STE) is a form of model checking fundamentally based on symbolic simulation. This article 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.'' The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

Logic and Metamathematics

• ACL2 verification of simplicial degeneracy programs in the Kenzo system, F.J. Martín-Mateos, J. Rubio and J.L. Ruiz-Reina. Calculemus 2009 - LNAI 5625, pp. 106-121, 2009. In this paper, we give a complete automated proof of the correctness of the encoding of degeneracy lists (a topological object) used in Kenzo, a Computer Algebra System devoted to Algebraic Topology.

• Formal Correctness of a Quadratic Unification Algorithm, J.L. Ruiz-Reina, F.J. Martín-Mateos, J.A. Alonso and M.J. Hidalgo. Journal of Automated Reasoning (37):1-2, pp. 67-92, 2006. The paper presents the formal verification of a syntactic unification algorithm of quadratic time complexity, using a dag representation for terms. The use of stobjs and defexec/mbe makes the algorithm efficiently executable.

• Proof Pearl: A Formal Proof of Higman's Lemma in ACL2, F.J. Martín-Mateos, J.L. Ruiz-Reina, J.A. Alonso and M.J. Hidalgo. TPHOLs 2005 - LNCS 3603, pp. 358-372, 2005. Highman's Lemma is a property about well quasi-orderings on strings. In this paper a formal proof of this result is presented, using a termination argument based on well-founded multiset extensions.

• A Formal Proof of Dickson's Lemma in ACL2, F.J. Martín-Mateos, J.A. Alonso, M.J. Hidalgo and J.L. Ruiz-Reina. LPAR 2003 - LNAI 2850, pp. 49-58, 2003. Dickson's Lemma is the main result needed for proving termination of Buchberger's algorithm for computing Gröbner basis of ideals of polynomials. In this paper a formal proof of this result is presented, using a termination argument based on well-founded multiset extensions.

• Formal verification of a generic framework to synthesize SAT-provers, F.J. Martín-Mateos, J.A. Alonso, M.J. Hidalgo and J.L. Ruiz-Reina. Journal of Automated Reasoning (32):4, pp. 287-313, 2004. A generic framework for SAT checkers is defined and verified. Several verified and executable SAT solvers can be obtained instantiating this generic framefork.

• Termination in ACL2 Using Multiset Relations, J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Martín-Mateos. Thirty Five Years of Automating Mathematics, pp. 217-245. 2003. A proof in ACL2 of the well-foundedness of multiset extensions of well-founded relations and a tool for generating automatically such multiset relations.

• A certified polynomial-based decision procedure for propositional logic , I. Medina Bulo, F. Palomo Lozano and J. A. Alonso Jiménez, 4th International Conference on Theorem Proving in Higher Order Logics , LNCS 2152:297-312. Edinburgh (Escocia), 2001. In this paper we present the formalization of a decision procedure for Propositional Logic based on polynomial normalization. This formalization is suitable for its automatic verification in an applicative logic like ACL2. This application of polynomials has been developed by reusing a previous work on polynomial rings, showing that a proper formalization leads to a high level of reusability. Two checkers are defined: the first for contradiction formulas and the second for tautology formulas. The main theorems state that both checkers are sound and complete. Moreover, functions for generating models and counterexamples of formulas are provided. This facility plays also an important role in the main proofs. Finally, it is shown that this allows for a highly automated proof development.

• Formal Proofs About Rewriting Using ACL2, J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Martín-Mateos. Annals of Mathematics and Artificial Intelligence 36(3), pp. 239-262, 2002. This paper presents a formalization of term rewriting systems. That is, ACL2 is used as the metatheory to formalize results in equational reasoning and rewrite systems. Notions such as confluence, local confluence, and normal forms are formalized. The main theorems proved are Newman's Lemma and Knuth-Bendix critical-pair theorem.

• Ivy: A Preprocessor and Proof Checker for First-Order Logic, William McCune and Olga Shumsky, Chapter 16 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

Miscellaneous Applications

• A verified Common Lisp implementation of Buchberger's algorithm in ACL2. I. Medina Bulo, F. Palomo Lozano, and J. L. Ruiz Reina. Journal of Symbolic Computation 45-1:96-123. 2010. In this article, we present the formal verification of a Common Lisp implementation of Buchberger's algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.

• Formal Verification of Molecular Computational Models in ACL2: A Case Study, F.J. Martín-Mateos, J.A. Alonso, M.J. Hidalgo and J.L. Ruiz-Reina. CAEPIA 2003 - LNCS 3040, pp. 344-353, 2004. A formalization in ACL2 of Lipton's experiment that uses DNA computation for solving SAT.

• Verified Computer Algebra in ACL2 (Gröbner Bases Computation), I. Medina Bulo, F. Palomo Lozano, J. A. Alonso Jiménez and J. L. Ruiz Reina, Artificial Intelligence and Symbolic Mathematical Computation (AISC 2004) , LNAI 3249:171-184. Linz (Austria), 2004. In this paper, we present the formal verification of a Common LISP implementation of Buchberger's algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in the ACL2 system and shows how verified Computer Algebra can be achieved in an executable logic.

• Verification of an In-place Quicksort in ACL2, Sandip Ray and Rob Sumners. In D. Borrione, M. Kaufmann, and J S. Moore, editors, Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002), Grenoble, France, April 2002, pages 204-212.

• A Mechanical Proof of the Chinese Remainder Theorem, David Russinoff, in Proceedings of ACL2 Workshop 2000.

• Knuth's Generalization of McCarthy's 91 Function, John Cowles, Chapter 17 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts) This article 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. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.

• Verification of Year 2000 Conversion Rules, Matt Kaufmann, March 1999 (revised from June 1999). This page links to event files in support of the paper "Verification of Year 2000 Conversion Rules Using the ACL2 Theorem Prover," to appear in Software Tools for Technology Transfer. This formal verification of COBOL transformation rules was done in support of Y2K remediation performed at EDS CIO Services using an in-house proprietary tool, Cogen 2000.
• A Mechanically Checked Proof of a Comparator Sort Algorithm, J Moore and B. Brock, in, M. Broy, J. Gruenbauer, D. Harel, and C. A. R. Hoare (eds.) Engineering Theories of Software Intensive Systems, Springer NATO Science Series II, 195, pp. 141-175, 2005. This paper describes a mechanically checked correctness proof for the comparator sort algorithm underlying a microcode program in a commercially designed digital signal processing chip. The abstract algorithm uses an unlimited number of systolic comparator modules to sort a stream of data. In addition to proving that the algorithm produces an ordered permutation of its input, two theorems are proved that are important to verifying the microcode implementation. These theorems describe how positive and negative ``infinities'' can be streamed into the array of comparators to achieve certain effects. Interesting generalizations are necessary in order to prove these theorems inductively. (ACL2 Script)

• The Specification of a Simple Autopilot in ACL2, Bill Young, July, 1996. This paper presents an ACL2 translation of Butler's PVS formalization of a simple autopilot.

Related Web Sites

• Mechanized Reasoning Database (USA)
• Mechanized Reasoning Database (Germany)
• Formal Methods
• ORA Canada Bibliography of Automated Deduction