ACL2 Workshop 2000

ACL2 Workshop 2000 was held Oct. 30-31, 2000 in the Governor's Room of the Texas Union, University of Texas at Austin, Austin, Texas. It was preceded by a brief tutorial on Sunday, Oct. 29. The workshop proceedings are available as UTCS Technical Report TR-00-29.

The organizers thank Jo O'Neil-Moore for her many significant contributions to the local arrangements for the workshop.



ACL2 is described at The previous year's workshop produced two books:

and includes articles by a number of contributors on topics ranging from real analysis and first-order logic to the mechanical verification of designs of industrial interest like an RTL description of a floating-point multiplier and the verification of a safety- critical component of a compiler.

We expect another ACL2 Workshop to take place in 2002, probably just before or just after a larger workshop or conference.

The ACL2 community gratefully acknowledges the support of Advanced Micro Devices, Inc., which has donated a gift to defray some of the costs of this year's workshop. Links are provided below to final copies of the accepted papers. In many cases there are also links to slides and to supporting materials, which are generally ACL2 script files or ``books'' to provide full details.


Sunday, October 29:
2:00 Informal gathering
2:30 - 6:00
Tutorial (break with refreshments, approx. 4:00 - 4:30)
Flying Demo
The Method
Monday, October 30:
Workshop, Day 1
8:30   Breakfast
9:00   Welcome
9:15 R. Lusk,
B. McCune
ACL2 for Parallel Systems Software: A Progress Report
(PDF) (PS) (Supporting materials)
9:40 M. Wilding Using a Single-Threaded Object to Speed a Verified Graph Pathfinder
(PDF) (PS)
10:20   Long break
10:45 R. Sumners Correctness Proof of a BDD Manager in the Context of Satisfiability Checking
(PDF) (PS) (Supporting materials) (Slides [PDF] [PS])
11:25   Lunch
1:15 O. Shumsky,
L. J. Henschen
Developing a Framework for Simulation, Verification and Testing of SDL Specifications
(PDF) (PS) (Slides [Power Point] [HTML])
1:40 P. Manolios Verification of Pipelined Machines in ACL2
(PDF) (PS) (Supporting materials)
2:20   Long break
2:45 R. Sumners An Incremental Stuttering Refinement Proof of a Concurrent Program in ACL2
(PDF) (PS) (Supporting materials) (Slides [PDF] [PS])
3:25   Break
3:40 J.-L. Ruiz-Reina,
J.-A. Alonso,
M.-J. Hidalgo,
F.-J. Martin
Multiset Relations: A Tool for Proving Termination
(PDF) (PS) (Supporting materials) (Slides [PS])
4:20   Break
4:35   Discussion: Work in progress, ACL2 directions, ACL2 wish lists
6:00   Close of first day.
Tuesday, October 31:
Workshop, Day 2
8:30   Breakfast
9:00 W. Goerigk Proving Preservation of Partial Correctness with ACL2: A Mechanical Compiler Source Level Correctness Proof
(PDF) (PS) (Slides [PDF])
9:40 J. Sawada ACL2 Computed Hints: Extension and Practice
(PDF) (PS)
10:05   Long break
10:30 I. Medina-Bulo,
J.A. Alonso-Jimenez,
F. Palomo-Lozano
Automatic Verification of Polynomial Rings: Fundamental Properties in ACL2
(PDF) (PS) (Supporting materials [HTML page] [gzipped tar file]) (Slides [PDF] [PS])
11:10 D. Russinoff A Mechanical Proof of the Chinese Remainder Theorem
(PDF) (PS) (Supporting materials) (Slides [PDF] [PS])
11:35   Lunch
1:25 P. Manolios,
J Moore
Partial Functions in ACL2
(PDF) (PS) (Supporting materials)
2:05   Discussion: next ACL2 Workshop, work in progress, ACL2 wish lists
2:35   Long break
3:00 T. Bailey,
J. Cowles
Knuth's Generalization of Takeuchi's Tarai Function: Preliminary Report
(PDF) (PS) (Supporting materials) (Slides [PDF] [PS])
3:40   Break
3:55 M. Kaufmann,
D. Russinoff
Verification of Pipeline Circuits
(PDF) (PS) (Supporting materials) (Slides [PS])
4:35   Break
4:50   Discussion: Work in progress, ACL2 directions, ACL2 wish lists
6:00   Close of second day.


Ken Albin
Flemming Andersen
Bill Bevier
Michael Bogomolny
Dominique Borrione
Bishop Brock
Inmaculada Medina Bulo
Yunja Choi
John Cowles
Warren E Ferguson
Art Flatau
Bob Gaebler
Ruben Gamboa
Philippe Georgelin
Wolfgang Goerigk
Dave Greve
John R Harrison
Warren A. Hunt Jr
Damir Jamsek
Abhijit Jas
Matt Kaufmann
Robert Bellarmine Krug
Wilfred Legato
Francisco Palomo Lozano
Peter Manolios
William McCune
J Strother Moore
Carlos Pacheco
Dana Pardubska
Laurence Pierre
Shaz Qadeer
Rajesh Radhakrishnan
Sanjai Rayadurgam
Jose L. Ruiz Reina
David Russinoff
Jun Sawada
Jodi Schneider
Olga Shumsky
Rob Sumners
Kong Woei Susanto
Elena Teica
Matthew Wilding


Bob Boyer (CS Department, University of Texas, Austin, Texas)
Piergiorgio Bertoli (IRST - Istituto per la Ricerca Scientifica e Tecnologica, Povo, Italy)
John Cowles (CS Department, University of Wyoming, Laramie, Wyoming)
Wolfgang Goerigk (IIPM, Christian-Albrechts-Universitat zu Kiel, Germany)
Matt Kaufmann (Advanced Micro Devices, Inc., Austin, Texas)
Pete Manolios (CS Department, University of Texas, Austin, Texas)
William McCune (MCS, Argonne National Laboratory, Argonne, Illinois)
J Moore (CS Department, University of Texas, Austin, Texas)
David Russinoff (Advanced Micro Devices, Inc., Austin, Texas)
Jun Sawada (IBM Austin Research Laboratory, Austin, Texas)
Matt Wilding (ATC, Rockwell Collins, Inc., Cedar Rapids, Iowa)


Matt Kaufmann (
J Moore (