\documentclass{article} \title{Bibtex Entries for the ACL2 Workshops} \author{Jared Davis} \begin{document} \maketitle This file provides a list of bibtex entries which can be used to cite papers from the ACL2 workshops from within \LaTeX{}. If you see any errors in these entries please email me at {\sf jared@cs.utexas.edu}. \section{ACL2 Workshop 2000} \noindent {\sf 00-lusk-parallel}\cite{00-lusk-parallel} \\ ACL2 for Parallel Systems Software: A Progress Report \\ \noindent {\sf 00-wilding-stobj}\cite{00-wilding-stobj} \\ Using a Single-Threaded Object to Speed a Verified Graph Pathfinder \\ \noindent {\sf 00-sumners-bdds}\cite{00-sumners-bdds} \\ Correcness Proof of a BDD Manager in the Context of Satisfiability Checking \\ \noindent {\sf 00-shumsky-sdl}\cite{00-shumsky-sdl} \\ Developing a Framework for Simulation, Verification and Testing of SDL Specifications \\ \noindent {\sf 00-manolios-pipeline}\cite{00-manolios-pipeline} \\ Verification of Pipelined Machines in ACL2 \\ \noindent {\sf 00-sumners-stuttering}\cite{00-sumners-stuttering} \\ An Incremental Stuttering Refinement Proof of a Concurrent Program in ACL2 \\ \noindent {\sf 00-reina-multiset}\cite{00-reina-multiset} \\ Multiset Relations: A Tool for Proving Termination \\ \noindent {\sf 00-goerigk}\cite{00-goerigk} \\ Proving Preservation of Partial Correctness with ACL2: A Mechanical Compiler Source Level Correctness Proof \\ \noindent {\sf 00-sawada-computed}\cite{00-sawada-computed} \\ ACL2 Computed Hints: Extension and Practice \\ \noindent {\sf 00-bulo-polynomial}\cite{00-bulo-polynomial} \\ Automatic Verification of Polynomial Rings: Fundamental Properties in ACL2 \\ \noindent {\sf 00-russinoff-chinese}\cite{00-russinoff-chinese} \\ A Mechanical Proof of the Chinese Remainder Theorem \\ \noindent {\sf 00-manolios-partial}\cite{00-manolios-partial} \\ Partial Functions in ACL2 \\ \noindent {\sf 00-bailey-tarai}\cite{00-bailey-tarai} \\ Knuth's Generalization of Takeuchi's Tarai Function: Preliminary Report \\ \noindent {\sf 00-kaufmann-pipeline}\cite{00-kaufmann-pipeline} \\ Verification of Pipeline Circuits \\ \section{ACL2 Workshop 2002} \noindent {\sf 02-barrione-vhdl}\cite{02-barrione-vhdl} \\ A Framework for VHDL Combining Theorem Proving and Symbolic Simulation \\ \noindent {\sf 02-caldwell-nuprl}\cite{02-caldwell-nuprl} \\ Representing Nuprl Proof Objects in ACL2: toward a proof checker for Nuprl \\ \noindent {\sf 02-sawada-sqrt}\cite{02-sawada-sqrt} \\ Formal Verification of Divide and Square Root Algorithms Using Series Calculation \\ \noindent {\sf 02-gamboa-taylor}\cite{02-gamboa-taylor} \\ Taylor's Formula with Remainder \\ \noindent {\sf 02-bulo-polynomial}\cite{02-bulo-polynomial} \\ Implementation in ACL2 of Well-Founded Polynomial Orderings \\ \noindent {\sf 02-reina-terms}\cite{02-reina-terms} \\ A Theory About First-Order Terms in ACL2 \\ \noindent {\sf 02-reina-dags}\cite{02-reina-dags} \\ Progress Report: Term Dags Using Stobjs \\ \noindent {\sf 02-manolios-adding}\cite{02-manolios-adding} \\ Adding a Total Order to ACL2 \\ \noindent {\sf 02-sumners-sat}\cite{02-sumners-sat} \\ Checking ACL2 Theorems via SAT Checking \\ \noindent {\sf 02-kaufmann-rewriting}\cite{02-kaufmann-rewriting} \\ Efficient Rewriting of Operations on Finite Structures in ACL2 \\ \noindent {\sf 02-cowles-primitive}\cite{02-cowles-primitive} \\ Consistently Adding Primitive Recursive Definitions in ACL2 \\ \noindent {\sf 02-cowles-flat}\cite{02-cowles-flat} \\ Flat Domains and Recursive Equations in ACL2 \\ \noindent {\sf 02-martin-molecular}\cite{02-martin-molecular} \\ Molecular Computation Models in ACL2: a Simulation of Lipton's Experiment Solving SAT \\ \noindent {\sf 02-martin-instantiation}\cite{02-martin-instantiation} \\ A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. \\ \noindent {\sf 02-ray-quicksort}\cite{02-ray-quicksort} \\ Verification of an In-place Quicksort in ACL2 \\ \section{ACL2 Workshop 2003} \noindent {\sf 03-kaufmann-simplifying}\cite{03-kaufmann-simplifying} \\ A Tool for Simplifying Files of ACL2 Definitions \\ \noindent {\sf 03-hendrix-matricies}\cite{03-hendrix-matricies} \\ Matricies in ACL2 \\ \noindent {\sf 03-manolios-ordinal}\cite{03-manolios-ordinal} \\ Ordinal Arithmetic in ACL2 \\ \noindent {\sf 03-sustik-dickson}\cite{03-sustik-dickson} \\ Proof of Dickson's Lemma Using the ACL2 Theorem Prover via an Explicit Ordinal Mapping \\ \noindent {\sf 03-gamboa-arrays}\cite{03-gamboa-arrays} \\ Using ACL2 Arrays to Formalize Matrix Algebra \\ \noindent {\sf 03-gamboa-kalman}\cite{03-gamboa-kalman} \\ On the Verification of Synthesized Kalman Filters \\ \noindent {\sf 03-matlin-encapsulation}\cite{03-matlin-encapsulation} \\ Encapsulation for Practical Simplification Procedures \\ \noindent {\sf 03-sumners-fairness}\cite{03-sumners-fairness} \\ Fair Environment Assumptions in ACL2 \\ \noindent {\sf 03-toma-sha}\cite{03-toma-sha} \\ SHA Formalization \\ \noindent {\sf 03-greve-separation}\cite{03-greve-separation} \\ A Separation Kernel Formal Security Policy \\ \noindent {\sf 03-moore-tagging}\cite{03-moore-tagging} \\ Memory Taggings and Dynamic Data Structures \\ \noindent {\sf 03-moore-assertions}\cite{03-moore-assertions} \\ Inductive Assertions and Operational Semantics \\ \noindent {\sf 03-greve-typed}\cite{03-greve-typed} \\ Typed ACL2 Records \\ \noindent {\sf 03-greve-mbe}\cite{03-greve-mbe} \\ Using MBE to Speed a Verified Graph Pathfinder \\ \noindent {\sf 03-liu-rockwell}\cite{03-liu-rockwell} \\ A Solution to the Rockwell Challenge \\ \noindent {\sf 03-song-security}\cite{03-song-security} \\ Using ACL2 to Verify Security Properties of Specification-based Intrusion Detection Systems \\ \noindent {\sf 03-al-sammane-mathematica}\cite{03-al-sammane-mathematica} \\ Combining ACL2 and Mathematica for the Symbolic Simulation of Digital Systems \\ \noindent {\sf 03-schmaltz-bus}\cite{03-schmaltz-bus} \\ Validation of a Parameterized Bus Architecture Model \\ \noindent {\sf 03-gamboa-polymorphism}\cite{03-gamboa-polymorphism} \\ Polymorphism in ACL2 \\ \noindent {\sf 03-gamboa-literate}\cite{03-gamboa-literate} \\ Writing Literate Proofs with XML Tools \\ \noindent {\sf 03-ray-modelchecking}\cite{03-ray-modelchecking} \\ Certifying Compositional Model Checking Algorithms in ACL2 \\ \noindent {\sf 03-austel-types}\cite{03-austel-types} \\ Implementing Abstract Types in ACL2 \\ \section{ACL2 Workshop 2004} \noindent {\sf 04-sumners-invariant}\cite{04-sumners-invariant} \\ Reducing Invariant Proofs to Finite Search via Rewriting \\ \noindent {\sf 04-ray-partial}\cite{04-ray-partial} \\ Attaching Efficient Executability to Partial Functions in ACL2 \\ \noindent {\sf 04-matthews-clock}\cite{04-matthews-clock} \\ Partial Clock Functions in ACL2 \\ \noindent {\sf 04-gameiro-interval}\cite{04-gameiro-interval} \\ Formally Verifying an Algorithm Based on Interval Arithmetic for Checking Transversality \\ \noindent {\sf 04-manolios-hard}\cite{04-manolios-hard} \\ A Suite of Hard ACL2 Theorems Arising in Refinement-Based Processor Verification \\ \noindent {\sf 04-davis-sets}\cite{04-davis-sets} \\ Finite Set Theory based on Fully Ordered Lists \\ \noindent {\sf 04-roach-hats}\cite{04-roach-hats} \\ Verifying Transformation Rules of the HATS High-Assurance Transformation System: An Approach \\ \noindent {\sf 04-fisler-features}\cite{04-fisler-features} \\ A Case Study in using ACL2 for Feature-Oriented Verification \\ \noindent {\sf 04-sawada-vhdl}\cite{04-sawada-vhdl} \\ ACL2VHDL Translator: A Simple Approach to Fill the Semantic Gap \\ \noindent {\sf 04-austel-typing}\cite{04-austel-typing} \\ Adding a typing mechanism to ACL2 \\ \noindent {\sf 04-reina-unification}\cite{04-reina-unification} \\ A Formally Verified Quadratic Unification Algorithm \\ \noindent {\sf 04-legato-preconditions}\cite{04-legato-preconditions} \\ Generic Theories as Proof Strategies: A Case Study for Weakest Precondition Style Proofs \\ \noindent {\sf 04-hunt-nonlinear}\cite{04-hunt-nonlinear} \\ Integrating Nonlinear Arithmetic into ACL2 \\ \noindent {\sf 04-greve-partitioning}\cite{04-greve-partitioning} \\ A Summary of Intrinsic Partitioning Verification \\ \noindent {\sf 04-greve-enumeration}\cite{04-greve-enumeration} \\ Address Enumeration and Reasoning Over Linear Address Spaces \\ \noindent {\sf 04-smith-bags}\cite{04-smith-bags} \\ An ACL2 Library for Bags (Multisets) \\ \noindent {\sf 04-richards-common}\cite{04-richards-common} \\ The Common Criteria, Formal Methods and ACL2 \\ \noindent {\sf 04-young-abstract}\cite{04-young-abstract} \\ Reverse Abstraction in ACL2 \\ \noindent {\sf 04-foss-gwv}\cite{04-foss-gwv} \\ An Analysis of the GWV Security Policy \\ \noindent {\sf 04-schmaltz-network}\cite{04-schmaltz-network} \\ A Functional Specification and Validation Model for Networks on Chip in the ACL2 Logic \\ \noindent {\sf 04-toma-sha}\cite{04-toma-sha} \\ Verification of a Cryptographic Circuit: SHA-1 using ACL2 \\ \noindent {\sf 04-gamboa-axiomatic}\cite{04-gamboa-axiomatic} \\ Axiomatic Events in ACL2(r): A Story of defun, defun-std, and encapsulate \\ \noindent {\sf 04-cowles-tail}\cite{04-cowles-tail} \\ Contributions to the Theory of Tail Recursive Functions \\ \bibliographystyle{plain} \bibliography{workshops} \end{document}