@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"
}