| Versions available | The current version available over the Net is 1.8. The release of Version 1.9 is pending approval from sponsoring agencies and should be out very soon. |
| Documentation available |
We have two browser-based ``
Tours'' to introduce you to ACL2, as well as a Tutorial. The paper ACL2 Theorems about Commercial Microprocessors (with Bishop Brock) briefly discusses the system and two ``industrial strength'' applications, the Motorola CAP project and the AMD5K86 floating point division project. See also Selected References. |
| Download Procedure |  |
| License Agreement | There is a single license agreement for all prospective users. |
| Freeware or fee structure | NA |