OSDN -- Desenvolver e Download de Software Open Source
Estado tradução de Português translation status for pt

RSS
Download List

Projeto Descrição

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

A solidez alguns bugs foram identificados e corrigidos, juntamente com vários potenciais erros Lisp rígido e outras questões menores. O desempenho dos invariantes teoria foi melhorada. Novos livros incluem uma resolução / provador paramodulation, modelagem de concorrência, indução transfinitos, e um utilitário de simplificação. Uma marca de confiança "" novo recurso permite a utilização dos recursos potencialmente inseguros em extensões 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 Download: Log de Alterações Download: Debian Package (deb) Download: Demo Home Page Download: List Download: TGZ