Proving Theorems About Java-Like Byte Code - Correct System Design: Recent Insights and Advances - page 155

6. R. M. Cohen, The Defensive Java Virtual Machine Specication, Version 0.53 ,
Electronic Data Systems, Corp, Austin Technical Services Center, 98 San
Jacinto Blvd, Suite 500, Austin, TX 78701 (email: [e-mail]).
7. A. D. Flatau, A veried implementation of an applicative language with dy-
namic storage allocation , PhD Thesis, University of Texas at Austin, 1992.
8. M. Kaufmann and J Strother Moore \An Industrial Strength Theorem Prover
for a Logic Based on Common Lisp," IEEE Transactions on Software Engi-
neering , 23 (4), pp. 203{213, April, 1997
9. M. Kaufmann and J Strother Moore \A Precise Description of
the ACL2 Logic," http://www.cs.utexas.edu/users/moore/publications/-
km97a.ps.Z, April, 1998.
10. T. Lindholm and F. Yellin The Java Virtual Machine Specication , Addison-
Wesley, 1996.
11. J S. Moore. Piton: A Mechanically Veried Assembly-Level Language .Auto-
mated Reasoning Series, Kluwer Academic Publishers, 1996.
12. G. L. Steele, Jr. Common Lisp The Language, Second Edition . Digital Press,
30 North Avenue, Burlington, MA 01803, 1990.
13. W. D. Young, A Veried Code-Generator for a Subset of Gypsy , PhD Thesis,
University of Texas at Austin" 1988.
14. Y. Yu. Automated Proofs of Object Code For a Widely Used Microproces-
sor . PhD thesis, University of Texas at Austin, 1992. Lecture Notes in
Computer Science, Springer-Verlag (to appear). ftp://ftp.cs.utexas.edu/pub-
/techreports/tr93-09.ps.Z.