OSDN -- Desarrollar y descargar software de código abierto
Translation Status of Español translation status for es

RSS
Download List

Descripción del Proyecto

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.

2006-12-05 09:07 Back to release list
3.1

Una solidez algunos bugs fueron identificados y corregidos junto con varios posibles errores Lisp duro y otras cuestiones de menor importancia. El rendimiento de la teoría de invariantes se ha mejorado. Nuevos libros incluyen una resolución / experimentador paramodulation, los modelos de concurrencia, la inducción transfinitos, y una utilidad de la simplificación. Una nueva "etiqueta de la confianza" permite el uso de características potencialmente peligrosas en las extensiones de ACL2.
Tags: Major bugfixes
A few soundness bugs were identified and corrected along with several potential hard Lisp errors and other minor issues. The performance of theory invariants has been improved. New books include a resolution/paramodulation prover, concurrency modelling, transfinite induction, and a simplification utility. A new "trust tag" feature allows the use of potentially unsafe features in ACL2 extensions.

Project Resources

Project Page Descargar: Changelog Descargar: Debian Package (deb) Descargar: Demo Página principal Descargar: List Descargar: TGZ