Top > All Packages in Directory > ACL2

ACL2 - Programming language for modelling computer systems and proving properties of those models

ACL2 is a mathematical logic and a mechanical theorem prover to help you reason in the logic (which is a subset of applicative Common Lisp). The theorem prover is an ``industrial strength'' version of the Boyer-Moore theorem prover, Nqthm. Users can build models of all kinds of computing systems in ACL2, just as in Nqthm, even though the formal logic is Lisp. Once you've built an ACL2 model of a system, you can run it and use ACL2 to prove theorems about the model.

Obtaining

Web pagehttp://www.cs.utexas.edu/users/moore/acl2/
Source tarballftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-7/acl2.tar.gz
Source information http://www.cs.utexas.edu/users/moore/acl2/v2-7/installation.html#Obtaining
Version 2.7 (stable) released on 2002-11-13
Licensed under The GNU General Public License, Version 2.
This is not a GNU package.

Documentation
User install guide available in HTML format from http://www.cs.utexas.edu/users/moore/acl2/v2-7/installation.html; User guide available in HTML format from http://www.cs.utexas.edu/users/moore/acl2/v2-7/The_Tours.html; Uer reference manual available in HTML format from http://www.cs.utexas.edu/users/moore/acl2/v2-7/#User's-Manual
Support contacts

Help List<acl2-help@lists.cc.utexas.edu> http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html
Developer List<acl2@lists.cc.utexas.edu> http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html
Bug List<acl2-bugs@lists.cc.utexas.edu> http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html

Project contacts

Maintainers
Developers
Sponsors
  • University of Texas at Austin

Related information

Interfacescommand line
Source languagesLisp
Related programsCLISP, Garnet, CMUCL, GCL

Entry information

License verified byJanet Casey <jcasey@gnu.org> on 2002-06-03
Entry compiled byJanet Casey <jcasey@gnu.org>

Categories


The copyright licensing notice below applies to this text. The software described in this text has its own copyright notice and license, which can usually be found in the distribution itself.

Copyright © 2000, 2001, 2002,2003 Free Software Foundation, Inc.

Permission is granted to copy, distribute, and/or modify this document under the terms of the GNU Free Documentation License, Version 1.1 or any later version published by the Free Software Foundation; with no Invariant Sections, with no Front-Cover Texts, and with no Back-Cover Texts. A copy of this license is included in the file COPYING.DOC.

Please report any problems in this page to bug-directory@gnu.org, or find out how you can help fix them.

The FSF provides this directory as a service to the free software community. Please consider donating to the FSF to help support this project.