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 http://www.cs.utexas.edu/users/moore/acl2. The previous
year's workshop produced two books:
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: 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. | |
| 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 |
| 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 | (matt.kaufmann@amd.com) |
| J Moore | (moore@cs.utexas.edu) |