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.

GENERAL INFORMATION
PRESENTATIONS
PARTICIPANTS
PROGRAM COMMITTEE
ORGANIZING COMMITTEE



GENERAL INFORMATION

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




PRESENTATIONS

Sunday, October 29:
Tutorial
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.



PARTICIPANTS

Ken Albin albin@lakewood.sps.mot.com
Flemming Andersen Flemming.L.Andersen@intel.com
Bill Bevier bbevier@eti.com
Michael Bogomolny bogo@cs.utexas.edu
Dominique Borrione Dominique.Borrione@imag.fr
Bishop Brock bcbrock@us.ibm.com
Inmaculada Medina Bulo inmaculada.medina@uca.es
Yunja Choi yuchoi@cs.umn.edu
John Cowles cowles@meru.cs.uwyo.edu
Warren E Ferguson warren.e.ferguson@intel.com
Art Flatau arthur.flatau@amd.com
Bob Gaebler rfgaeble@collins.rockwell.com
Ruben Gamboa ruben@acm.org
Philippe Georgelin Philippe.Georgelin@imag.fr
Wolfgang Goerigk wg@informatik.uni-kiel.de
Dave Greve dagreve@collins.rockwell.com
John R Harrison johnh@ichips.intel.com
Warren A. Hunt Jr whunt@austin.ibm.com
Damir Jamsek damir@austin.ibm.com
Abhijit Jas jas@ece.utexas.edu
Matt Kaufmann matt.kaufmann@amd.com
Robert Bellarmine Krug rkrug@cs.utexas.edu
Wilfred Legato legato@nsa.gov
Francisco Palomo Lozano Francisco.Palomo@uca.es
Peter Manolios pete@cs.utexas.edu
William McCune mccune@mcs.anl.gov
J Strother Moore moore@cs.utexas.edu
Carlos Pacheco pacheco@cs.utexas.edu
Dana Pardubska Dana.Pardubska@fmph.uniba.sk
Laurence Pierre Laurence.Pierre@cmi.univ-mrs.fr
Shaz Qadeer qadeer@pa.dec.com
Rajesh Radhakrishnan rradh@yahoo.com
Sanjai Rayadurgam rsanjai@cs.umn.edu
Jose L. Ruiz Reina jruiz@cica.es
David Russinoff david.russinoff@amd.com
Jun Sawada sawada@us.ibm.com
Jodi Schneider jodi@fireant.ma.utexas.edu
Olga Shumsky shumsky@ece.nwu.edu
Rob Sumners robert.sumners@amd.com
Kong Woei Susanto susanto@dcs.gla.ac.uk
Elena Teica eteica@ececs.uc.edu
Matthew Wilding mmwildin@collins.rockwell.com




PROGRAM COMMITTEE

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)



ORGANIZING COMMITTEE

Matt Kaufmann (matt.kaufmann@amd.com)
J Moore (moore@cs.utexas.edu)