Fourth International Workshop on the ACL2 Theorem Prover
and Its Applications (ACL2-2003)



The next ACL2 Workshop will be held July 13-14, 2003, in Boulder, Colorado, USA, in conjunction with (and immediately following) CAV. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend.

LOCATION. The room for the workshop will be ECCR 1B55. That's in the Engineering Center Complex, which on the east end of campus, on the southwest corner of Regent Dr. and Colorado Ave. Room 1B55 is at the northeast corner of the first basement level of the Classroom Wing of the Engineering Center Complex.

DINNER. There will be a dinner Sunday night, July 13, the cost of which is included in the registration fee:
The Taj, 2630 Baseline Rd. (at Broadway) -- show up between 7:00 and 7:30 pm.

ACL2 is a state-of-the-art automated reasoning system. It grew out of the Boyer-Moore theorem prover and has been used successfully on a number of industrial and academic projects. ACL2 is described at

The ACL2 workshops provide a forum for presentation and discussion of projects using ACL2 as well as evolution of the tool. Information about the preceding workshops, including slides, papers, and supporting materials, is available on-line:

The first workshop resulted in two books:


You can use one of the links to reservation forms, below, if you wish to reserve a dormitory room. (Email and postal addresses and costs are on the forms.) We have been told the following information about these rooms:

In case you want a double room, note that spouses not attending the workshop are best listed under Guest. Attendees who want to room together should each fill out the form and indicate their choice to share a room with each other in the "Roommate name" field. There are twin beds in all the rooms and the rooms are non-smoking and also not air conditioned. According to, the average temperatures in Boulder in July (Fahrenheit) are 87 high, 56 low.

Dorm reservation forms in various formats:

CAV has reserved a block of rooms at the Millenium Hotel through July 12, which apparently is 100 yards from campus. The rate is $112 per night (single or double occupancy) plus tax (total: $122.92). The hotel says that we can mention Computer-Aided Verification (CAV) and get that rate through as far as the night of July 14. Their phone number is 800-545-6285 (on the web:
Note: If you want a room there at that rate you may want to reserve it soon, as they claim that July is a busy month.


A good starting point for local information is:

One can follow links from that page to find transportation options from the Denver airport. Two such options appear to be as follows.


We invite papers on any topic related to ACL2, including but not limited to:

You can assume that the audience has a working knowledge of ACL2, including familiarity with the syntax, the basic commands, and modeling techniques used.

We are looking for papers of no more than about 20 pages in length. Papers of at most about 5 pages will generally be considered for "short talks" (probably 20 or 25 minutes), and others will be considered for "long talks" (probably 30 or 40 minutes). However, authors are encouraged to state explicitly their preference for giving a short or long talk. Note that short talks may report on work in progress, challenge problems, clever tricks, and so on.

Papers will be refereed by members of the Program Committee.

Submissions should be sent by email to Matt Kaufmann ( in Postscript and/or PDF format. Papers that describe successful uses of ACL2 should be accompanied by ordinary text files containing the appropriate ACL2 input and instructions for how to process them with ACL2, although the papers themselves should be self-contained.

We expect that accepted papers (both full and short) will be presented at the workshop and published in a conference proceedings format, perhaps on-line. Final copies of the papers will be collected shortly after the meeting.

Supporting materials. Where applicable, we encourage authors of accepted papers to provide ACL2 script files or ``books'' to provide full details, which can be mirrored on the ACL2 home page (above) and included in future ACL2 distributions. Please see the instructions for supporting materials.


Submission Deadline April 8, 2003 [extended from original date of April 1]
Acceptance Notification May 8, 2003 [extended from original date of May 1]
Last day to send in registration without late fee June 1, 2003
Final Papers Due July 7, 2003
Workshop July 13-14, 2003


Please fill out the registration form and send it, with a check, as directed on that page. The fee goes up after June 1.


NOTE: Copies of the schedule below (day1 and day2) will be available at the workshop.

Sunday, July 13:
Workshop, Day 1
8:30 Breakfast
9:00 Welcome
9:10 Matt Kaufmann A Tool for Simplifying Files of ACL2 Definitions
[PDF] [PS] [Supporting materials] (Slide handouts: [PDF] [PS]) (Slides (full-size): [PDF] [PS])
9:40 Joe Hendrix Matrices in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
10:00 Panagiotis Manolios
Daron Vroon (speaker)
Ordinal Arithmetic in ACL2
[PDF] [PS]
10:30 Long break (refreshments)
11:10 Matyas Sustik Proof of Dickson's Lemma Using the ACL2 Theorem Prover via an Explicit Ordinal Mapping
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
11:40 John Cowles (speaker),
Ruben Gamboa,
Jeff Van Baalen
Using ACL2 Arrrays to Formalize Matrix Algebra
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
12:00 Ruben Gamboa (speaker),
John Cowles,
Jeff Van Baalen
On the Verification of Synthesized Kalman Filters
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
12:30 Lunch
14:30 Olga Shumsky Matlin (speaker),
William McCune
Encapsulation for Practical Simplification Procedures
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS] [PowerPoint])
14:50 Rob Sumners Fair Environment Assumptions in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
15:10 Diana Toma (speaker),
Dominique Borrione
SHA Formalization
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
15:30 Long break (refreshments)
16:10 David Greve,
Matthew Wilding (speaker),
W. Mark Vanfleet
A Separation Kernel Formal Security Policy
[PDF] [PS] [Supporting materials]
16:40 Matt Kaufmann,
J Moore
What's new in ACL2; General Discussion (e.g., ACL2 enhancement requests)
[Talk notes (plain text)]
18:00 End of first day
Monday, July 14:
Workshop, Day 2
8:30 Breakfast
9:00 Announcements
9:10 J Strother Moore Memory Taggings and Dynamic Data Structures
[PDF] [PS] [Supporting materials]
9:40 J Strother Moore Inductive Assertions and Operational Semantics -- Long Version
[PDF] [PS] [Supporting materials]
10:10 Short break
10:25 David Greve (speaker),
Matthew Wilding
Typed ACL2 Records
[PDF] [PS] [Supporting materials]
10:45 David Greve (speaker),
Matthew Wilding
Using MBE to Speed a Verified Graph Pathfinder
[PDF] [PS] [Supporting materials]
11:05 Long break (refreshments)
11:35 Hanbing Liu A Solution to the Rockwell Challenge
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]))
12:05 Tao Song (speaker),
Jim Alves-Foss,
Calvin Ko,
Cui Zhang,
Karl Levitt
Using ACL2 to Verify Security Properties of Specification-based Intrusion Detection Systems
[PDF] [PS] [Supporting materials]
12:25 Lunch
14:25 Julien Schmaltz,
Ghiath Al Sammane,
Dominique Borrione,
Pierre Ostier,
Diana Toma (speaker)
Combining ACL2 and Mathematica for the Symbolic Simulation of Digital Systems
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
14:45 Julien Schmaltz (speaker),
Dominique Borrione
Validation of a parameterized bus architecture using ACL2
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])
15:05 Short break
15:20 Ruben Gamboa (speaker),
Mark Patterson
Polymorphism in ACL2
[PDF] [PS] (Slides: [PDF])
15:50 Ruben Gamboa Writing Literate Proofs with XML Tools
[PDF] [PS] [Supporting materials page] (Slides: [PDF])
16:10 Long break (refreshments)
16:40 Sandip Ray (speaker),
John Matthews,
Mark Tuttle
Certifying Compositional Model Checking Algorithms in ACL2
[PDF] [PS] [Supporting materials] (Slide handouts: [PDF] [PS]) (Slides (full-size): [PDF] [PS])
17:10 Vernon Austel Implementing abstract types in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PDF] [PS (gzipped)])
17:30   General Discussion (ACL2 enhancements, time/place of next workshop)
18:00 Workshop ends




Austel, Vernon IBM
Cowles, John Univ. of Wyoming
Fedeli, Andrea
Gamboa, Ruben Univ. of Wyoming
Greve, Dave Rockwell Collins
Harrison, John Intel
Hendrix, Joe Univ. of Illinois at Urbana-Champaign
Hunt, Warren Univ. of Texas at Austin
Kaufmann, Matt AMD
Kuzmina, Nadya Univ. of Wyoming
Legato, Wilfred U.S. Govt.
Liu, Hanbing Univ. of Texas at Austin
Manolios, Pete Georgia Tech Univ.
Matlin, Olga Shumsky Argonne National Labs.
Moore, J Univ. of Texas at Austin
Patterson, Mark Univ. of Wyoming
Ray, Sandip Univ. of Texas at Austin
Reeber, Erik Univ. of Texas at Austin
Richards, Ray Rockwell Collins
Roach, Steve Univ. of Texas at El Paso
Schmaltz, Julien TIMA Laboratory, Grenoble, France
Smith, Eric AMD / Stanford Univ.
Song, Tao Univ. of California at Davis
Sumners, Rob AMD
Sustik, Matyas Univ. of Texas at Austin
Toma, Diana TIMA Laboratory, Grenoble, France
Van Groningen, Serita Rockwell Collins / Univ. of Texas at Austin
Vroon, Daron Georgia Tech Univ.
Wilding, Matthew Rockwell Collins