@Book{kmm00a,
 author	   = {M. Kaufmann and P. Manolios and J S. Moore},
 title     = "{Computer-Aided Reasoning:  An Approach}",
 publisher = "Kluwer Academic Press",
 address   = "Boston, MA.",
 year      = "2000"
}

@Book{kmm00b,
 editor    = {M. Kaufmann and P. Manolios and J S. Moore},
 title     = "{Computer-Aided Reasoning:  {ACL2} Case Studies}",
 publisher = "Kluwer Academic Press",
 address   = "Boston, MA.",
 year      = "2000"
}

@Article{russinoff98,
 author    = "D. Russinoff",
 title     = "A Mechanically Checked Proof of {IEEE} Compliance of
              a Register-Transfer-Level Specification of the {AMD-K7}
              Floating-Point Multiplication, Division, and Square 
              Root Instructions",
 journal   = "London Mathematical Society Journal of
              Computation and Mathematics",
 volume    = "1",
 pages     = "148--200",
 month     = "December",
 year      = "1998",
 note      = "http://www.onr.com/user/russ/david/k7-div-sqrt.html"}

@inproceedings{kmm00b-chap13,
 title     ="RTL Verification: A Floating-Point Multiplier",
 author    ="D. M. Russinoff and A. Flatau",
 pages     ="201--232",
 editor    = {M. Kaufmann and P. Manolios and J S. Moore},
 booktitle = "{Computer-Aided Reasoning:  {ACL2} Case Studies}",
 publisher = "Kluwer Academic Press",
 address   = "Boston, MA.",
 year      = "2000"
}

@article{mlk98,
 key       ="Moore, Lynch, Kaufmann",
 author    ="J S. Moore and T. Lynch and M. Kaufmann",
 title     ="A Mechanically Checked Proof of the Correctness of the
             Kernel of the {AMD5K86} Floating Point Division Algorithm",
 journal   ="IEEE Transactions on Computers",
 volume    ="47",
 number    ="9",
 pages     ="913--926",
 month     ="September",
 year      ="1998"
}

@incollection{Sawada02,
 author    ="J. Sawada",
 title     ="Formal Verification of Divide and Square Root Algorithms
             Using Series Calculation",
 booktitle ="Proceedings of the ACL2 Workshop, 2002",
 editors   ="D. Borrione, M. Kaufmann, J S. Moore",
 publisher ="\url{http://www.cs.utexas.edu/users/moore/acl2/workshop-2002}",
 address   ="Grenoble",
 month     ="April",
 year      ="2002"
}

@incollection{bh99,
 author    ={B. Brock and Hunt, Jr., W. A.},
 title     ="Formal Analysis of the Motorola {CAP} {DSP}",
 booktitle ="Industrial-Strength Formal Methods",
 editors   ="Mike Hinchey and Jonathan Bowen",
 publisher ="Springer-Verlag",
 year      ="1999"
}

@inproceedings{bm05,
 author    ="B. Brock and J S. Moore",
 title     ="A Mechanically Checked Proof of a Comparator Sort Algorithm",
 publisher ="IOS Press, Amsterdam",
 editors   ="C. A. R. Hoare and D. Harel and M. Broy",
 booktitle ="Engineering Theories of Software Intensive Systems",
 year      ="2005 (to appear)"
}

@misc{gw03,
 author    = "David Greve and M. Wilding",
 title     = "A Separation Kernel Formal Security Policy",
 publisher = "\url{citeseer.ist.psu.edu/greve03separation.html}",
 year      ="2003"
}

@inproceedings{moore02a,
 author    ="J S. Moore",
 title     ="Proving Theorems about {Java} and the {JVM} with {ACL2}",
 booktitle ="Models, Algebras and Logic of Engineering Software",
 publisher ="IOS Press, Amsterdam",
 editor    ="M. Broy and M. Pizka",
 year      ="2003",
 pages     ="227--290",
 note      ="http://www.cs.utexas.edu/users/moore/publications/marktoberdorf-03"
}

@inproceedings{lm03,
 author    ="H. Liu and J S. Moore",
 title     ="Executable {JVM} Model for Analytical Reasoning: A Study",
 booktitle ="Workshop on Interpreters, Virtual Machines
             and Emulators 2003 (IVME '03)",
 publisher ="ACM SIGPLAN",
 address   ="San Diego, CA",
 month     ="June",
 year      ="2003"
}

@inproceedings{sumners00,
 author    ="R. Sumners",
 title     ="Correctness Proof of a {BDD} Manager in the Context
             of Satisfiability Checking",
 booktitle ="Proceedings of ACL2 Workshop 2000",
 editors   ="M. Kaufmann and J S. Moore",
 publisher ="Department of Computer Sciences, Technical Report TR-00-29",
 month     ="November",
 year      ="2000",
 note      ="\url{http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/final/sumners2/paper.ps}"
}

@inproceedings{kmm00b-chap16,
 author    ="W. McCune and O. Shumsky",
 title     ="Ivy: A Preprocessor and Proof Checker for First-Order Logic",
 pages     ="265--282",
 editor    = {M. Kaufmann and P. Manolios and J S. Moore},
 booktitle = "{Computer-Aided Reasoning:  {ACL2} Case Studies}",
 publisher = "Kluwer Academic Press",
 address   = "Boston, MA.",
 year      = "2000"
}

@inproceedings{km,
 author    ="M. Kaufmann and J S. Moore",
 title     ="The {ACL2} Home Page",
 booktitle ="\url{http://www.cs.utexas.edu/users/moore/acl2/}",
 publisher ="Dept. of Computer Sciences, University of Texas at Austin",
 year      ="2004"
}

@inproceedings{kmm00b-chap6,
 author    ="M. Kaufmann",
 title     ="Modular Proof: The Fundamental Theorem of Calculus",
 pages     ="75--92",
 editor    = {M. Kaufmann and P. Manolios and J S. Moore},
 booktitle = "{Computer-Aided Reasoning:  {ACL2} Case Studies}",
 publisher = "Kluwer Academic Press",
 address   = "Boston, MA.",
 year      = "2000"
}


@inproceedings{km97a,
 author    = "M. Kaufmann and J S. Moore",
 title     = "A Precise Description of the {ACL2} Logic",
 booktitle = "\url{http://www.cs.utexas.edu/users/moore/publications/km97a.ps.gz}",
 publisher = "Dept. of Computer Sciences,
              University of Texas at Austin",
 year      = "1997"
}

@article{kp96,
 author    ="M. Kaufmann and P. Pecchiari",
 title     ="Interaction with the Boyer-Moore Theorem Prover:
             A Tutorial Study Using the Arithmetic-Geometric Mean Theorem",
 journal   ="Journal of Automated Reasoning",
 volume    ="16",
 number    ="1--2",
 year      ="1996",
 pages     ="181--222"
}