ACL2 Version 6.1 News

Table of Contents

• VSTTE 2012 Competition
• ACL2 Books Repository
• Performance Comparisons
• ACL2 Course Materials

This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.

Performance Comparisons

The statistics below correspond to runs of make ACL2_JOBS=8 regression using community books (available from the acl2-books project website), skipping directory books/clause-processors/SULFA/, for ACL2 executables built on Linux platforms as indicated. Not shown are results of testing on Windows and Mac OS X. Each regression was run on Ubuntu Linux.

64-bit ACL2 Linux runs on 3.5 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading, using make ACL2_JOBS=8

• CCL Version 1.9-dev-r15542M-trunk:

  21441.020u 673.790s 1:04:39.14 570.0%	0+0k 234608+1315736io 768pf+0w

• Lispworks Version 6.1.1:

  23007.590u 447.510s 1:08:33.47 570.2%	0+0k 0+1382848io 0pf+0w

• Gnu Common Lisp (GCL) Version 2.6.8pre, 1048576 maximum pages:

  24748.380u 794.960s 1:11:16.18 597.3%	0+0k 111144+3359312io 0pf+0w

• SBCL Version 1.1.4:

  26047.770u 539.310s 1:19:39.55 556.2%	0+0k 440864+1647352io 1385pf+0w

• Allegro CL Version 9.0:

  27708.360u 490.800s 1:27:20.94 538.0%	0+0k 0+1483824io 0pf+0w

64-bit ACL2(h) Linux runs on 3.5 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading, using make ACL2_JOBS=8

• CCL Version 1.9-dev-r15542M-trunk:

  23729.300u 1261.790s 1:19:04.96 526.6%	0+0k 168+1550192io 0pf+0w

• Lispworks Version 6.1.1 [Note: Skipped models/y86 because of insufficient values for array-dimension-limit and for array-dimension-limit.]:

  25299.000u 507.560s 1:21:53.34 525.2%	0+0k 0+1533992io 0pf+0w

• SBCL Version 1.1.4:

  29354.590u 817.940s 1:34:42.05 531.0%	0+0k 499552+1834872io 1447pf+0w

• Allegro CL Version 9.0:

  34136.440u 565.450s 2:07:49.23 452.4%	0+0k 199352+1645720io 674pf+0w

32-bit ACL2 Linux runs on 2.8 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading, using make ACL2_JOBS=8

• Gnu Common Lisp (GCL) Version 2.6.8pre, 524288 maximum pages:

  29908.985u 710.528s 1:33:28.86 545.9%	0+0k 69800+3164088io 0pf+0w

• CCL Version 1.9-dev-r15542M-trunk:

  34357.779u 509.415s 1:44:45.70 554.7%	0+0k 10064+1310624io 1pf+0w

• CMU Common Lisp (CMUCL) Version 19e:

  79225.199u 1170.889s 4:02:15.93 553.0%	0+0k 179648+1601920io 507pf+0w

ACL2 Course Materials

• CSU 290 Spring 2009 at Northeastern.
• The following two interfaces to ACL2 support the teaching of ACL2 to undergraduates:
  • The ACL2 Sedan (ACL2s)
  • DrACuLa
• Here is a link to the web page for Yishai Feldman's Computer-Aided Reasoning course at The Interdisciplinary Center, Herzliya.
• John Cowles, COSC5010: Formalizing the JVM in ACL2, Univ. of Wyoming.
• Links to some of Warren Hunt's courses, many of which use ACL2, may be found here.
• Logic and Computation, a freshman class taught by Pete Manolios and Riccardo Pucella at Northeastern.
• Here are links to web pages for courses taught by Pete Manolios at Georgia Tech:
  • CS 8803 Computational Logic (Spring 2005)
  • CS 8001 Hardware Verification Fall 2004
  • CS 3220 Processor Design.
• Links to some of J Moore's courses, many of which use ACL2, may be found here.
• A course taught by Rex Page at the Univ. of Oklahoma, and related links.
• Eric Smith's web page for a class at Stanford