MIME-Version: 1.0 Server: CERN/3.0 Date: Monday, 06-Jan-97 21:39:36 GMT Content-Type: text/html Content-Length: 4568 Last-Modified: Wednesday, 04-Sep-96 03:37:07 GMT ACL2 Version 1.9 ACL2


ACL2 Version 1.9

Copyright (C) 1989-96 Computational Logic, Inc. (CLI). All rights reserved.

ACL2 is a programming language in which you can model computer hardware and software, as well as a tool to help you prove properties of those models.


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.

We have two Web browser ``Tours'' to introduce you to ACL2, as well as a Tutorial.

To obtain ACL2

Matt Kaufmann and J Strother Moore

September 3, 1996

Selected References

Images

If your machine is listed below, you can avoid rebuilding ACL2 by obtaining a binary image. You should nevertheless read the License Agreement and obtain the Sources and Documentation. Then download the appropriate image and follow the QUICK AND EASY INSTALLATION INSTRUCTIONS in Installation Instructions.