ACL2 Version 8.4 News

Table of Contents


A soundness bug involves the use of SATISFIES type-specs in defstobj events. A patch, with explanation, is available here.


The "changelogs" for ACL2 are in the release-notes topics of the manuals. In particular, there are release notes for Version 8.4.

ACL2 sources availability between releases

ACL2 sources are available between releases at the ACL2 GitHub Repository.

VSTTE 2012 Competition

A team of four ACL2 users entered the VSTTE 2012 competition. For information, including the team's solution, visit this link.

ACL2 Books Repository

The ACL2 GitHub repository allows contributions of ACL2 books (input files), and also provides between-release updates.

Performance Comparisons

We have not put up performance comparison information for ACL2 Version 8.4. Feel free to see the performance comparisons page for ACL2 Version 8.3.