ACL2 Version 6.1 ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award. SEARCH

	Start Here: Applications, Tours, and Tutorials/Demos		ACL2 Workshops and UT ACL2 Seminar
	Books and Papers about ACL2 and Its Applications		The User's Manual and Hyper-Card
	Lemma Libraries and Utilities		Mailing Lists
	Recent changes to this page		Obtaining, Installing, and License
	Differences from Version 6.0		Other Releases
	How to contribute libraries and documentation

• ACL2(r)
  Support for the real numbers by way of non-standard analysis
  Ruben Gamboa
• ACL2(h)
  Support for hash cons, applicative hash tables, and function memoization for reuse of previously computed results
  Bob Boyer, Warren A. Hunt, Jr., Jared Davis, and Sol Swords
• ACL2(p)
  Support for parallel evaluation
  David L. Rager

There are libraries of books (files containing definitions and theorems) that extend the code that we have written. Books are contributed and maintained by the ACL2 community (see http://acl2-books.googlecode.com/; in particular, the [Source] tab near the top takes you to a search box) and their authors are generally noted in each book or its README file. There is a combined manual that incorporates not only The User's Manual for ACL2 but also documentation for many books; thanks to Jared Davis for building this view of the documentation.

Another extension of ACL2 is the Eclipse-based ACL2 Sedan (ACL2s). Unlike the systems above, ACL2s is distributed and maintained by Pete Manolios and his research group. ACL2s comes with a standard executable ACL2 image for Windows, but it also comes with pre-certified community books and an extension of ACL2 with additional features, including extra automation for termination proofs as well as counterexample generation.

• DARPA
• National Science Foundation
  • This material is based upon work supported by the National Science Foundation under Grant Nos. EIA-0303609, CNS-0429591, ISS-0417413, CCF-0945316, and CNS-0910913.
  • Any opinions, findings and conclusions or recomendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.
• Advanced Micro Devices, Inc.
• ForrestHunt, Inc.
• Rockwell Collins, Inc.
• Sun Microsystems, Inc.

The User's Manual

Here are the two common entries to the documentation graph:

	Major Topics (Table of Contents)
	Index of all documented topics

The tiny warning signs, , indicate that the links lead out of introductory level material and into reference manual material. Once in the reference manual, virtually all links are into the manual and none of them is marked with the warning sign! It is easy for the newcomer to get lost.

Here is how we recommend you use this documentation.

If you are a newcomer to ACL2, we do not recommend that you wander off into the full documentation. Instead start with the ACL2-TUTORIAL documentation topic. Experienced users tend mostly to use the ``Index'' to look up concepts mentioned in error messages or vaguely remembered from their past experiences with ACL2.

Note: The documentation is available for reading in a Web browser (recommended), in Emacs Info, using the ACL2 :DOC command, or as a printed book (over 2100 pages). These are available as follows.

• For web browsing using an HTML version of our documentation, click on Major Topics (here, or above). Better yet, view a local copy, which you can find under your local acl2-sources/ diretory at doc/HTML/acl2-doc.html.
• Alternatively, for web browsing you can use documentation generated by Jared Davis's xdoc utility. After you install and certify the ACL2 community books (see below), you will find a complete local copy at books/xdoc-impl/manual/preview.html.
• Those familiar with Emacs Info can read the documentation in that format by loading the file emacs/emacs-acl2.el distributed with ACL2 (under the acl2-sources directory), and then evaluating meta-x acl2-info. Alternatively, within Emacs Info press g and then enter the following path (of course, replacing PATH_TO_ACL2-SOURCES by the path of your acl2-sources directory):
  (PATH_TO_ACL2-SOURCES/doc/EMACS/acl2-doc-emacs.info)top.
• To read a printed copy, obtain a Postscript version here (about 2.5 MB).

Lemma Libraries and Utilities; and, How to Contribute

We strongly encourage users to submit additional books by following the instructions for contributing books to ACL2.

We also distribute a few interface tools, such as support for infix printing. For these, see the Utilities section of Books and Papers about ACL2 and Its Applications. Some of the papers mentioned in that collection contain utilities, scripts, or ACL2 books for the problem domains in question.

How to contribute libraries and documentation

Also, if you have written up (or are interested in writing) text that may be helpful to other ACL2 users, we invite you to contribute it to the community. Such user documentation may be in any format that is readable by web browsers (for example html, pdf, and plain text). User-contributed documentation can link back to the ACL2 documentation proper, by using links such as:
http://www.cs.utexas.edu/users/moore/acl2/current/MAKE-EVENT.html
(In general, substitute the upper-case of the documentation topic for "MAKE-EVENT" in the example above.)

To contribute user documentation, send email to the ACL2 developers, Matt Kaufmann and J Strother Moore.

Searching documentation and books

• The following link will take you to a search box on a Google page, which has the following contents.

  search_term site:http://www.cs.utexas.edu/users/moore/acl2/v6-1
  

  Now simply replace the word `search_term' with your topic. For example, replace `search_term' by `tail recursion' to get documentation about tail recursion.

  tail recursion site:http://www.cs.utexas.edu/users/moore/acl2/v6-1
  

  Now you are ready to follow the link.

  SEARCH THE DOCUMENTATION

• The next link will take you to the community books website (which is external to the present ACL2 website), spefically to the section entitled ``Searching and browsing the books.'' There, you will see a search box in which you can enter your search term. For example, if you type `tail recursion' and then <RETURN>, you will see text from several books in the svn trunk that deal with the topic of tail recursion, with an accompanying ``File Path'' shown at the end of each book's text.

  SEARCH THE COMMUNITY BOOKS