ACL2 Workshop 2000 was held Oct. 30-31, 2000 in the Governor's
Room of the Texas Union, University of Texas at Austin, Austin,
| R. Lusk, B. McCune |
ACL2 for Parallel Systems Software:
A Progress Report PostScript |
| M. Wilding | Using a Single-Threaded Object to
Speed a Verified Graph Pathfinder PostScript |
| R. Sumners | Correctness Proof of a BDD Manager
in the Context of Satisfiability Checking PostScript Slides in PostScript |
| P. Manolios | Verification of Pipelined Machines
in ACL2 PostScript |
| O. Shumsky, L. J. Henschen |
Developing a Framework for
Simulation, Verification and Testing of SDL Specifications PostScript |
| R. Sumners | An Incremental Stuttering Refinement
Proof of a Concurrent Program in ACL2 PostScript Slides in PostScript |
| J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, F.-J. Martin |
Multiset Relations: A Tool for Proving
Termination PostScript Slides in PostScript |
| W. Goerigk | Proving Preservation of Partial Correctness
with ACL2: A Mechanical Compiler Source Level Correctness Proof PostScript |
| J. Sawada | ACL2 Computed Hints: Extension and
Practice PostScript |
| I. Medina-Bulo, J.A. Alonso-Jimenez, F. Palomo-Lozano |
Automatic Verification of Polynomial
Rings: Fundamental Properties in ACL2 PostScript Slides in PostScript |
| D. Russinoff | A Mechanical Proof of the Chinese
Remainder Theorem PostScript Slides in PostScript |
| P. Manolios, J Moore |
Partial Functions in ACL2 PostScript |
| T. Bailey, J. Cowles |
Knuth's Generalization of Takeuchi's
Tarai Function: Preliminary Report PostScript |
| M. Kaufmann, D. Russinoff |
Verification of Pipeline Circuits PostScript Slides in PostScript |