Fifth International Workshop on the ACL2 Theorem Prover
and Its Applications (ACL2-2004)



The next ACL2 Workshop will be held November 18-19, 2004, in Austin, Texas, USA, in conjunction with (and immediately following) FMCAD 2004. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend.

The workshop will take place in room 2.402 of the ACES (Applied Computational Engineering and Sciences Building) building, at the University of Texas at Austin, at the corner of 24th Street and Speedway.

DINNER. There will be a dinner, the cost of which is included in the registration fee for participants, who can register dinner guests at an extra $30 each. Details:

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:


PARKING. If you wish to drive to campus and want the workshop to validate your parking, please send email no later than November 12 to Jo Moore ( stating that. We will assume you'll want to park one car for both days of the workshop and make suitable arrangements. Only those people who contact Jo no later than November 12 will have their parking validated. Parking will be in the San Jacinto garage, on the east side of San Jacinto Blvd. between 24th and 26th streets.

For the lodging options below, if you would like rides to and from the workshop, feel free to email Matt Kaufmann ( and we'll see what we can do.

Those attending FMCAD may wish to continue to stay at the Hyatt, which is about 2 1/2 miles from the ACES building. You can walk about 3/10 of a mile from there to a bus that will take you to Guadalupe at 24th, about 2 blocks from the ACES building. There are however more reasonably-priced alternatives, including the following.


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 before the meeting and may be revised shortly afterwards. We encourage authors to submit their papers to journals to reach a wider audience when appropriate, subject of course to copyright issues in case we find a conventional publisher for the proceedings.

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: August 2, 2004
Acceptance Notification: August 30, 2004
Last day to send in registration without late fee: October 14, 2004
Final Papers Due: November 8, 2004
Workshop: November 18-19, 2004


Registration is being handled through the FMCAD registration site, This will allow you to register for the ACL2 workshop without registering for FMCAD, if that is your preference. (Note: One successful registration on August 29 resulted in an email confirmation that included a URL. When reading that email on a Linux box in emacs, that URL needed to be edited, deleting =<return> and also replacing =3D by =.)

The above site will allow you buy extra T-shirts and/or purchase extra Thursday night dinners. Note that the last day to register without a late fee is October 15, 2004.


1.Copies of the schedule and of slides will be available at the workshop.
2. Additional links to papers and slides will continue to appear below.

For the printer:

Thursday, November 18:
Workshop, Day 1
8:30 Breakfast
9:00 Welcome
  Session 1 (Chair: Matt Kaufmann)
9:05 Rob Sumners (speaker),
Sandip Ray
Reducing Invariant Proofs to Finite Search via Rewriting
[Paper] [Slides] [Supporting materials]
9:35 Sandip Ray Attaching Efficient Executability to Partial Functions in ACL2
[Paper] [Slides] [Supporting materials]
9:55 John Matthews (speaker),
Daron Vroon
Partial Clock Functions in ACL2
[Paper] [Slides] [Supporting materials]
10:25 Long break
  Session 2 (Chair: Vernon Austel)
10:55 Marcio Gameiro (speaker),
Panagiotis Manolios
Formally Verifying an Algorithm Based on Interval Arithmetic for Checking Transversality
[Paper] [Slides] [Supporting materials]
11:25 Panagiotis Manolios,
Sudarshan K. Srinivasan (speaker)
A Suite of Hard ACL2 Theorems Arising in Refinement-Based Processor Verification
[Paper] [Slides] [Supporting materials]
11:45 Jared Davis Finite Set Theory based on Fully Ordered Lists
[Paper] [Slides] [Supporting materials]
12:15 Lunch
  Session 3 (Chair: Jose Luis Ruiz-Reina)
14:00 Steve Roach,
Fares Fraij (speaker)
Verifying Transformation Rules of the HATS High-Assurance Transformation System: An Approach
[Paper] [Slides] [Supporting materials]
14:20 Kathi Fisler (speaker),
Brian Roberts
A Case Study in using ACL2 for Feature-Oriented Verification
[Paper] [Slides] [Supporting materials (for ACL2 Version 2.5)]
14:40 Matt Kaufmann,
J Moore,
ACL2 Directions
[Discussion topics]
15:10 Long break
  Session 4 (Chair: Warren Hunt)
15:40 Jun Sawada ACL2VHDL Translator: A Simple Approach to Fill the Semantic Gap
[Paper] [Slides] [Supporting materials]
16:10 Vernon Austel Adding a typing mechanism to ACL2
[Paper] [Slides] [Note: No supporting materials]
16:30 Short break
  Session 5 (Chair: Pete Manolios)
16:50 J.L. Ruiz Reina (speaker),
J.A. Alonso,
M.J. Hidalgo,
F.J. Martin-Mateos
A Formally Verified Quadratic Unification Algorithm
[Paper] [Slides] [Supporting materials]
17:20 ALL General Discussion (e.g., ACL2 enhancements)
18:00 End of first day
Friday, November 19:
Workshop, Day 2
8:30 Breakfast
9:00 Welcome
  Session 6 (Chair: J Moore)
9:05 Wilfred Legato Generic Theories as Proof Strategies: A Case Study for Weakest Precondition Style Proofs
[Paper] [Appendix] [Slides] [Reference [7]] [Supporting materials]
9:35 Warren A Hunt, Jr.,
Robert Bellarmine Krug (speaker),
J Moore
Integrating Nonlinear Arithmetic into ACL2
[Paper] [Slides] [Note: No supporting materials]
10:05 Short break
  Session 7 (Chair: Ruben Gamboa)
10:25 David Greve,
Raymond Richards,
Matthew Wilding (speaker)
A Summary of Intrinsic Partitioning Verification
[Paper] [Note: No slides or supporting materials]
10:55 David Greve Address Enumeration and Reasoning Over Linear Address Spaces
[Paper] [Note: No slides] [Supporting materials]
11:25 Long break
  Session 8 (Chair: Robert Krug)
11:55 Eric Smith (speaker),
Serita Nelesen,
David Greve,
Matthew Wilding,
Raymond Richards
An ACL2 Library for Bags (Multisets)
[Paper] [Slides as delivered] [Slides with more details][Supporting materials]
12:15 Raymond Richards (speaker),
David Greve,
Matthew Wilding,
W. Mark Vanfleet
The Common Criteria, Formal Methods and ACL2
[Paper] [Note: No slides or supporting materials]
12:35 Lunch
  Session 9 (Chair: Dave Greve)
14:20 Bill Young Reverse Abstraction in ACL2
[Paper] [Slides]
14:40 Jim Alves-Foss,
Carol Taylor (speaker)
An Analysis of the GWV Security Policy
[Paper] [Slides]
15:00 Short break
  Session 10 (Chair: Anna Slobodova)
15:15 Julien Schmaltz (speaker),
Dominique Borrione
A Functional Specification and Validation Model for Networks on Chip in the ACL2 Logic
[Paper] [Slides] [Supporting materials]
15:45 Diana Toma (speaker),
Dominique Borrione
Verification of a cryptographic circuit: SHA-1 using ACL2
[Paper] [Slides]
16:05 Long break
  Session 11 (Chair: Jun Sawada)
16:35 John Cowles,
Ruben Gamboa (speaker),
Nadya Kuzmina
Axiomatic Events in ACL2(r): A Story of defun, defun-std, and encapsulate
[Paper] [Slides] [Note: No supporting materials]
17:05 John Cowles (speaker),
Ruben Gamboa
Contributions to the Theory of Tail Recursive Functions
[Paper] [Slides] [Supporting materials]
17:25 ALL General Discussion (e.g., ACL2 enhancements and time/place of next workshop)
18:00 Workshop ends




The list of participants is in this pdf file.