% ACL2 Workshop 2000 ===========================================================

@techreport{00-lusk-parallel,
  author="Ewing Lusk and William McCune",
  title="{ACL2} for Parallel Systems Software: A Progress Report",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-wilding-stobj,
  author="Matthew Wilding",
  title="Using a Single-Threaded Object to Speed a Verified Graph Pathfinder",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-sumners-bdds,
  author="Rob Sumners",
  title="Correcness Proof of a {BDD} Manager in the Context of Satisfiability Checking",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
} 

@techreport{00-shumsky-sdl,
  author="Olga Shumsky and Lawrence J. Henschen",
  title="Developing a Framework for Simulation, Verification and Testing of {SDL} Specifications",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
} 

@techreport{00-manolios-pipeline,
  author="Panagiotis Manolios",
  title="Verification of Pipelined Machines in {ACL2}",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
} 

@techreport{00-sumners-stuttering,
  author="Rob Sumners",
  title="An Incremental Stuttering Refinement Proof of a Concurrent Program in {ACL2}",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
} 

@techreport{00-reina-multiset,
  author="J. L. Ruiz-Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in",
  title="Multiset Relations: A Tool for Proving Termination",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
} 

@techreport{00-goerigk,
  author="Wolfgang Goerigk",
  title="Proving Preservation of Partial Correctness with {ACL2}: A Mechanical Compiler Source Level Correctness Proof",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-sawada-computed,
  author="Jun Sawada",
  title="{ACL2} Computed Hints: Extension and Practice",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-bulo-polynomial,
  author="I. Medina-Bulo and J. A. Alonso-Jim\'enez and F. Palomo-Lozano",
  title="Automatic Verification of Polynomial Rings: Fundamental Properties in {ACL2}",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-russinoff-chinese,
  author="David M. Russinoff",
  title="A Mechanical Proof of the {Chinese} Remainder Theorem",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-manolios-partial,
  author="Panagiotis Manolios and J Strother Moore",
  title="Partial Functions in {ACL2}",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-bailey-tarai,
  author="Tom Bailey and John Cowles",
  title="Knuth's Generalization of {Takeuchi's} {Tarai} Function: Preliminary Report",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-kaufmann-pipeline,
  author="Matt Kaufmann and David M. Russinoff",
  title="Verification of Pipeline Circuits",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}


% ACL2 Workshop 2002 ===========================================================

@inproceedings{02-barrione-vhdl,
  author="Philippe Georgelin and Dominique Borrione and Pierre Ostier",
  title="A Framework for {VHDL} Combining Theorem Proving and Symbolic Simulation",
  booktitle="Third International Workshop on the {ACL2} Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-caldwell-nuprl,
  author="James L. Caldwell and John Cowles",
  title="Representing {Nuprl} Proof Objects in {ACL2}: toward a proof checker for {Nuprl}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-sawada-sqrt,
  author="Jun Sawada",
  title="Formal Verification of Divide and Square Root Algorithms Using Series Calculation",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-gamboa-taylor,
  author="Ruben A. Gamboa and Brittany Middleton",
  title="Taylor's Formula with Remainder",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-bulo-polynomial,
  author="I. Medina-Bulo and F. Palomo-Lozano and J. A. Alonso-Jim\'enez",
  title="Implementation in {ACL2} of Well-Founded Polynomial Orderings",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-reina-terms,
  author="J. L. Ruiz-Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in-Mateos",
  title="A Theory About First-Order Terms in {ACL2}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-reina-dags,
  author="J. L. Ruiz-Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in-Mateos",
  title="Progress Report: Term Dags Using Stobjs",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-manolios-adding,
  author="Panagiotis Manolios and Matt Kaufmann",
  title="Adding a Total Order to {ACL2}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-sumners-sat,
  author="Rob Sumners",
  title="Checking {ACL2} Theorems via {SAT} Checking",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-kaufmann-rewriting,
  author="Matt Kaufmann and Rob Sumners",
  title="Efficient Rewriting of Operations on Finite Structures in {ACL2}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-cowles-primitive,
  author="John Cowles",
  title="Consistently Adding Primitive Recursive Definitions in {ACL2}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-cowles-flat,
  author="John Cowles",
  title="Flat Domains and Recursive Equations in {ACL2}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-martin-molecular,
  author="F. J. Mart\'in-Mateos and J. A. Alonso and M. J. P\'erez-Jim\'enez and F. Sancho-Caparrini",
  title="Molecular Computation Models in {ACL2}: a Simulation of {Lipton's} Experiment Solving {SAT}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-martin-instantiation,
  author="F. J. Mart\'{i}n-Mateos and J. A. Alonso and M. J. Hidalgo and J. L. Ruiz-Reina",
  title="A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}

@inproceedings{02-ray-quicksort,
  author="Sandip Ray and Rob Sumners",
  title="Verification of an In-place Quicksort in {ACL2}",
  booktitle="Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
  month="April",
  year="2002"
}


% ACL2 Workshop 2003 ===========================================================

@inproceedings{03-kaufmann-simplifying,
  author="Matt Kaufmann",
  title="A Tool for Simplifying Files of {ACL2} Definitions",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-hendrix-matricies,
  author="Joe Hendrix",
  title="Matricies in {ACL2}",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-manolios-ordinal,
  author="Panagiotis Manolios and Daron Vroon",
  title="Ordinal Arithmetic in {ACL2}",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-sustik-dickson,
  author="Matyas Sustik",
  title="Proof of {Dickson's} Lemma Using the {ACL2} Theorem Prover via an Explicit Ordinal Mapping",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-gamboa-arrays,
  author="Ruben Gamboa and John Cowles and Jeff Van Baalen",
  title="Using {ACL2} Arrays to Formalize Matrix Algebra",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-gamboa-kalman,
  author="Ruben Gamboa and John Cowles and Jeff Van Baalen",
  title="On the Verification of Synthesized {Kalman} Filters",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-matlin-encapsulation,
  author="Olga Shumsky Matlin and William McCune",
  title="Encapsulation for Practical Simplification Procedures",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-sumners-fairness,
  author="Rob Sumners",
  title="Fair Environment Assumptions in {ACL2}",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-toma-sha,
  author="Diana Toma and Dominique Borrione",
  title="{SHA} Formalization",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-greve-separation,
  author="David Greve and Matthew Wilding and W. Mark Vanfleet",
  title="A Separation Kernel Formal Security Policy",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-moore-tagging,
  author="J Strother Moore",
  title="Memory Taggings and Dynamic Data Structures",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-moore-assertions,
  author="J Strother Moore",
  title="Inductive Assertions and Operational Semantics",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-greve-typed,
  author="David Greve and Matthew Wilding",
  title="Typed {ACL2} Records",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-greve-mbe,
  author="David Greve and Matthew Wilding",
  title="Using {MBE} to Speed a Verified Graph Pathfinder",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-liu-rockwell,
  author="Hanbing Liu",
  title="A Solution to the {Rockwell} Challenge",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-song-security,
  author="Tao Song and Jim Alves-Foss and Calvin Ko and Cui Zhang and Karl Levitt",
  title="Using {ACL2} to Verify Security Properties of Specification-based Intrusion Detection Systems",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-al-sammane-mathematica,
  author="Ghiath Al Sammane and Dominique Borrione and Pierre Ostier and Julien Schmaltz and Diana Toma",
  title="Combining {ACL2} and {Mathematica} for the Symbolic Simulation of Digital Systems",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-schmaltz-bus,
  author="Julien Schmaltz and Dominique Borrione",
  title="Validation of a Parameterized Bus Architecture Model",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-gamboa-polymorphism,
  author="Ruben Gamboa and Mark Patterson",
  title="Polymorphism in {ACL2}",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}


@inproceedings{03-gamboa-literate,
  author="Ruben Gamboa",
  title="Writing Literate Proofs with {XML} Tools",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-ray-modelchecking,
  author="Sandip Ray and John Matthews and Mark Tuttle",
  title="Certifying Compositional Model Checking Algorithms in {ACL2}",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}

@inproceedings{03-austel-types,
  author="Vernon Austel",
  title="Implementing Abstract Types in {ACL2}",
  booktitle="Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03)",
  month="July",
  year="2003"
}


% ACL2 Workshop 2004 ===========================================================

@inproceedings{04-sumners-invariant,
  author="Rob Sumners and Sandip Ray",
  title="Reducing Invariant Proofs to Finite Search via Rewriting",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-ray-partial,
  author="Sandip Ray",
  title="Attaching Efficient Executability to Partial Functions in {ACL2}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-matthews-clock,
  author="John Matthews and Daron Vroon",
  title="Partial Clock Functions in {ACL2}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-gameiro-interval,
  author="Marcio Gameiro and Panagiotis Manolios",
  title="Formally Verifying an Algorithm Based on Interval Arithmetic for Checking Transversality",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}


@inproceedings{04-manolios-hard,
  author="Panagiotis Manolios and Sudarshan K. Srinivasan",
  title="A Suite of Hard {ACL2} Theorems Arising in Refinement-Based Processor Verification",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-davis-sets,
  author="Jared Davis",
  title="Finite Set Theory based on Fully Ordered Lists",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-roach-hats,
  author="Steve Roach and Fares Fraij",
  title="Verifying Transformation Rules of the {HATS} High-Assurance Transformation System: An Approach",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-fisler-features,
  author="Kathi Fisler and Brian Roberts",
  title="A Case Study in using {ACL2} for Feature-Oriented Verification",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-sawada-vhdl,
  author="Jun Sawada",
  title="{ACL2VHDL} Translator: A Simple Approach to Fill the Semantic Gap",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-austel-typing,
  author="Vernon Austel",
  title="Adding a typing mechanism to {ACL2}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04)",
  month="November",
  year="2004"
}

@inproceedings{04-reina-unification,
  author="J. L. Ruiz Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in-Mateos",
  title="A Formally Verified Quadratic Unification Algorithm",
  booktitle="Fifth International Workshop on the {ACL2} Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-legato-preconditions,
  author="Wilfred Legato",
  title="Generic Theories as Proof Strategies: A Case Study for Weakest Precondition Style Proofs",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-hunt-nonlinear,
  author="Warren A. {Hunt, Jr.} and Robert Bellarmine Krug and J Moore",
  title="Integrating Nonlinear Arithmetic into {ACL2}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-greve-partitioning,
  author="David Greve and Raymond Richards and Matthew Wilding",
  title="A Summary of Intrinsic Partitioning Verification",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-greve-enumeration,
  author="David Greve",
  title="Address Enumeration and Reasoning Over Linear Address Spaces",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-smith-bags,
  author="Eric Smith and Serita Nelesen and David Greve and Matthew Wilding and Raymond Richards",
  title="An {ACL2} Library for Bags (Multisets)",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-richards-common,
  author="Raymond Richards and David Greve and Matthew Wilding",
  title="The {Common Criteria}, Formal Methods and {ACL2}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-young-abstract,
  author="Bill Young",
  title="Reverse Abstraction in {ACL2}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-foss-gwv,
  author="Jim Alves-Foss and Carol Taylor",
  title="An Analysis of the {GWV} Security Policy",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-schmaltz-network,
  author="Julien Schmaltz and Dominique Borrione",
  title="A Functional Specification and Validation Model for Networks on Chip in the {ACL2} Logic",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-toma-sha,
  author="Diana Toma and Dominique Borrione",
  title="Verification of a Cryptographic Circuit: {SHA-1} using {ACL2}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-gamboa-axiomatic,
  author="Ruben Gamboa and John Cowles and Nadya Kuzmina",
  title="Axiomatic Events in {ACL2(r)}: A Story of defun, defun-std, and encapsulate",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}

@inproceedings{04-cowles-tail,
  author="John Cowles and Ruben Gamboa",
  title="Contributions to the Theory of Tail Recursive Functions",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '04)",
  year="2004",
  month="November"
}