Bibliography

ACL205

ACL2 home page.
www.cs.utexas.edu/users/moore/acl2/.

BOO51

BOOTH, A.D., A Signed Binary Multiplication Technique, Quart. J. Mech. Appl. Math. 4, Part 2, 1951.

GAM99

GAMBOA, REUBEN, Mechanically Verifying Real-Valued Algorithms in ACL2, Ph.D. dissertation, Dept. of Computer Sciences, U. of Texas at Austin, May, 1999.

IEEE85

INSTITUTE OF ELECTRICAL AND ELECTRONIC ENGINEERS, IEEE Standard for Binary Floating Point Arithmetic, Std. 754-1985, New York, NY, 1985.

KAU00a

KAUFMANN, M., P. MANOLIOS, AND J S. MOORE, Computer-Aided Reasoning: An Approach. Kluwer Academic Press, 2000.

KAU00b

KAUFMANN, M., P. MANOLIOS, AND J S. MOORE, editors, Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, 2000.

KAU00d

KAUFMANN, M. AND D. M. RUSSINOFF, Verification of pipeline circuits, Proceedings ACL2 Workshop 2000, Oct. 2000.
www.cs.utexas.edu/users/moore/acl2/workshop-2000/.

KAU03

KAUFMANN, M., A tool for simplifying files of ACL2 definitions, Proceedings ACL2 Workshop 2003, July 2003.
www.cs.utexas.edu/users/moore/acl2/workshop-2003/.

KLI72

KLINE, MORRIS, Mathematical Thought from Ancient to Modern Times, Oxford University Press, 1972.

KOR93

KOREN, ISRAEL, Computer Arithmetic Algorithms, 2nd edition, A.K. Peters, 1993.

MOO98

MOORE, J, T. LYNCH, AND M. KAUFMANN, A mechanically checked proof of the correctness of the kernel of the floating point division algorithm, IEEE Transactions on Computers, 47:9, September, 1998.

RUS98

RUSSINOFF, D.M., A mechanically checked proof of IEEE compliance of the AMD-K7 floating point multiplication, division, and square root instructions, London Mathematical Society Journal of Computation and Mathematics (1), 148-200, December, 1998.
www.russinoff.com/papers/k7-div-sqrt.html.

RUS99

RUSSINOFF, D.M., A mechanically checked proof of IEEE compliance of the AMD-K5 floating point square root microcode, Formal Methods in System Design 14, 75-125 (1999).
www.russinoff.com/papers/fsqrt.html.

RUS00a

RUSSINOFF, D.M., A case study in formal verification of register-transfer logic with ACL2: the floating point adder of the AMD Athlon processor, invited paper, FMCAD 2000.
www.russinoff.com/papers/fadd.html.

RUS00b

RUSSINOFF, D.M. AND A. FLATAU, RTL verification: a floating-point multiplier, in [KAU00b], pp. 201-232.
www.russinoff.com/papers/acl2.html.

STE90

STEELE, G.L., JR., Common Lisp The Language, 2nd edition, Digital Press, 1990.