OSDN -- Develop and Download Open Source Software

RSS
Download List

Project Description

ACL2 is a mathematical logic, programming
language, and mechanical theorem prover based on
the applicative subset of Common Lisp. It is an
"industrial-strength" version of the NQTHM or
Boyer/Moore theorem prover, and has been used for
the formal verification of commercial
microprocessors, the Java Virtual Machine,
interesting algorithms, and so forth.

System Requirements

System requirement is not defined
Information regarding Project Releases and Project Resources. Note that the information here is a quote from Freecode.com page, and the downloads themselves may not be hosted on OSDN.

2005-04-23 08:41
2.9.2

This release added a simple system for saving ACL2 images with "preloaded" theories and support for profiling your ACL2 functions using GCL (with gprof). Minor cleanups were made in the ground zero theory, several lemmas were added to the RTL books, and the system call mechanism for portable output redirection was improved. Untranslate preprocessing was added along with a new book that provides pattern-based untranslation. Various (non-soundness) bugfixes related to guards, linear arithmetic, the proof checker, and the ground zero theory were made.
Tags: Minor feature enhancements

2004-12-23 00:22
2.9.1

Tags: Initial freshmeat announcement

Project Resources

Project Page Download: Changelog Download: Debian Package (deb) Download: Demo Home Page Download: List Download: TGZ