Download List


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 requirement is not defined
Information regarding Project Releases and Project Resources. Note that the information here is a quote from page, and the downloads themselves may not be hosted on OSDN.

2009-05-26 06:08

There is improved support for controlling the printer and "eviscerating" large objects. Certificate files now take advantage of structure sharing and are more compact. The user now has more control over the "rulers" used in termination analysis. Many various efficiency improvements have been made, mainly with respect to supporting very large objects. A few soundness bugs have been patched, and there have been numerous other bugfixes.

2007-06-05 23:51

标签: Minor feature enhancements
A soundness bug and some other minor bugs have been fixed. Including books has been sped up by as much as 50%. Rewriting can be dynamically monitored. Accumulated persistence supports meta-rules and identifies useless rules, and many other minor updates have been made.

2006-12-05 09:07

标签: 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.

2006-08-06 06:07

标签: Minor feature enhancements
Several bugs were fixed, including a soundness bug. Efficiency has been significantly improved, and the regression suite runs about 20% faster. New features include time limits for the prover, enhanced controls for compilation with certify-book, and a new utility for debugging failed encapsulate and progn events.

2006-06-01 09:54

一个新的化妆活动的特点是引入。这几乎是一样的宏采取的状态。提供了更好的支持为:定义规则:扩大线索。禁用增加了警卫检查。用户贡献的书籍现在支持,以及各种各样的功能得到改善,其中包括后卫核查涉及地面条件,不变量理论和diabling defthm事件。阿健全错误与某些地方活动已得到修复,由于有轻微的化学武器有关的错误,gstack,湿,可嵌入的事件,及时,证明树木,stobj印刷和:吹嘘。
标签: Major feature enhancements
A new make-event feature was introduced. It is almost like macros that take state. Better support was provided for :definition rules with :expand hints. Disabling guard checking was added. User-contributed books are now supported, and a variety of features have been improved, including guard verification involving ground terms, theory invariants, and diabling defthm events. A soundness bug related to certain local events has been fixed, as have minor bugs related to cw-gstack, wet, embeddable events, the prompt, proof trees, stobj printing, and :puff.

Project Resources