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 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
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.