ACL2 3.1 review

ACL2 is a programming language in which you can model computer systems and a tool to help you prove properties of those models

License: GPL (GNU General Public License) File size: 6571K Developer: Matt Kaufmann and J S. Moore

0

ACL2 is a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 stands for "A Computational Logic for Applicative 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.

What's New in This Release:
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.