About-ACL2
General information About ACL2
This is ACL2 Version 8.6, copyright (C) 2025,
Regents of the University of Texas, authored by Matt Kaufmann and J Strother
Moore.
See the ACL2 home
page for additional information including tutorials, installation
instructions, mailing lists, related publications, ACL2 workshops and
seminars, acknowledgments, and other ACL2 releases.
See documentation for how to access the ACL2 User's Manual.
For statistics on ACL2 code size, see file doc/acl2-code-size.txt.
Subtopics
- Recursion-and-induction
- Recursion and Induction
- Operational-semantics
- Modeling State Machines
- Soundness
- Correctness property claimed for ACL2
- Release-notes
- Pointers to what has changed
- Version
- ACL2 Version Number
- Acknowledgments
- Some contributors to the well-being of ACL2
- Pre-built-binary-distributions
- Pre-built binary distributions of ACL2
- Common-lisp
- Relation to Common Lisp, including deviations from the spec
- Git-quick-start
- Git quick start guide
- Copyright
- ACL2 copyright, license, sponsorship
- Building-ACL2
- How to build an ACL2 executable
- ACL2-help
- The acl2-help mailing list
- Bibliography
- Reports about ACL2
