OSDN -- 开发和下载开源软件
简体中文翻译状态 translation status for zh

RSS
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 Freecode.com page, and the downloads themselves may not be hosted on OSDN.

2009-05-26 06:08 Back to release list
3.5

有改进控制打印机和“去脏”大型对象的支持。现在证书文件共享的结构优势，更为紧凑。用户现在有更多的对“在分析中使用的统治者终止”控制。许多不同的效率，改善工作已经完成，主要是就支持非常大的对象。一些稳健的错误已被修复，并有许多其他错误修正。
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.

Project Resources

Project Page 下载: 变更日志 下载: Debian Package (deb) 下载: Demo 首页 下载: List 下载: TGZ