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

GENERAL INFORMATION TRANSPORTATION AND LODGING CALL FOR PAPERS DATES REGISTRATION PRESENTATIONS PROGRAM COMMITTEE ORGANIZING COMMITTEE PARTICIPANTS LIST

GENERAL INFORMATION

LOCATION.
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:

• Time: Thursday night, November 18, 7:30 pm (feel free to come early to hang out; there will be a cash bar).
• Place: Serrano's, 1111 Red River St. (next to Symphony Square).
• Food: Fajitas (beef, chicken, and vegetarian).

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 http://www.cs.utexas.edu/users/moore/acl2.

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:

• ACL2 Workshop 1999 March 29 - March 31, 1999, Austin, TX, USA.
• ACL2 Workshop 2000 October 30-31, 2000, Austin, TX, USA.
• ACL2 Workshop 2002 April 8-9, 2002, Grenoble, France.
• ACL2 Workshop 2003 July 13-14, 2003, Boulder, CO, USA.

• Computer-Aided Reasoning: An Approach, Kaufmann, Manolios, Moore, Kluwer (June, 2000)
• Computer-Aided Reasoning: ACL2 Case Studies, Kaufmann, Manolios, Moore (eds), Kluwer (June, 2000)

TRANSPORTATION AND LODGING

For the lodging options below, if you would like rides to and from the workshop, feel free to email Matt Kaufmann (kaufmann@cs.utexas.edu) 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.

• The Austin Motel
  This is about 3 miles from the ACES building, and is on a bus line that will get you about 2 blocks from ACES.
• Holiday Inn Town Lake
  This is about 4 miles from the ACES building. They have a shuttle that will get you at least to 15th and Red River, which is still about 1.2 miles from the ACES building.

CALL FOR PAPERS

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

• applications of the theorem prover
• improvements and extensions to the theorem prover
• comparisons of ACL2 to other theorem provers, programming languages, or specification languages
• solved challenge problems for ACL2 users (especially challenges that help newcomers learn the system)
• implementations connecting ACL2 and other systems

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 (kaufmann@cs.utexas.edu) 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.

DATES

REGISTRATION

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.

PRESENTATIONS

NOTE:
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:

• Day 1 schedule only
• Day 2 schedule only

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, ALL	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

PROGRAM COMMITTEE

• Vernon Austel (IBM)
• Ruben Gamboa (Univ. of Wyoming)
• Dave Greve (Rockwell Collins)
• Mike Gordon (Univ. of Cambridge)
• Warren Hunt (University of Texas, Austin)
• Matt Kaufmann (Advanced Micro Devices)
• Robert Krug (University of Texas, Austin)
• Pete Manolios (Georgia Institute of Technology)
• J Moore (University of Texas, Austin)
• Jose Luis Ruiz-Reina (Universidad de Sevilla)
• Jun Sawada (IBM)
• Anna Slobodova (Intel)

ORGANIZING COMMITTEE

• Matt Kaufmann (kaufmann@cs.utexas.edu)
• J Moore (moore@cs.utexas.edu)

PARTICIPANTS LIST