ACL2 3.1 reviewDownload
ACL2 is a programming language in which you can model computer systems and a tool to help you prove properties of those models
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.
ACL2 3.1 keywords