Bibliography

1

W.R. Bevier, W.A. Hunt, J S. Moore, and W.D. Young.
Special issue on system verification.
Journal of Automated Reasoning, 5(4):409-530, 1989.

2

E. Borger and W. Schulte.
Defining the java virtual machine as platform for provably correct java compilation.
In Proceedings of MFCS'98, volume LNCS 1450, pages 17-35. Springer, 1998.

3

R. S. Boyer and J S. Moore.
A Computational Logic.
Academic Press, New York, 1979.

4

R. S. Boyer and J S. Moore.
Mechanized formal reasoning about programs and computing machines.
In R. Veroff, editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pages 147-176. MIT Press, 1996.

5

R. S. Boyer and J S. Moore.
A Computational Logic Handbook, Second Edition.
Academic Press, New York, 1997.

6

Robert S. Boyer and Yuan Yu.
Automated proofs of object code for a widely used microprocessor.
Journal of the ACM, 43(1):166-192, January 1996.

7

R. M. Cohen.
The defensive Java Virtual Machine specification, version 0.53.
Technical report, Electronic Data Systems Corp, Austin Technical Services Center, 98 San Jacinto Blvd, Suite 500, Austin, TX 78701, 1997.

8

A. D. Flatau.
A verified implementation of an applicative language with dynamic storage allocation.
Phd thesis, University of Texas at Austin, 1992.

9

J. Gosling, B. Joy, and G. Steele.
The Java Language Specification.
Addison-Wesley, 1996.

10

P. Haggar.
Practical Java Programming Language Guide.
Addison-Wesley, 2000.

11

David Hardin, Matthew Wilding, and David Greve.
Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle.
In Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided Verification - CAV '98, volume 1427 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
See URL https://pobox.com/users/hokie/docs/concept.ps.

12

M. Kaufmann, P. Manolios, and J S. Moore, editors.
Computer-Aided Reasoning: ACL2 Case Studies.
Kluwer Academic Press, 2000.

13

M. Kaufmann, P. Manolios, and J S. Moore.
Computer-Aided Reasoning: An Approach.
Kluwer Academic Press, 2000.

14

T. Lindholm and F. Yellin.
The Java Virtual Machine Specification (Second Edition).
Addison-Wesley, 1999.

15

J S. Moore.
Proving theorems about Java-like byte code.
In E.-R. Olderog and B. Steffen, editors, Correct System Design - Recent Insights and Advances, pages 139-162. LNCS 1710, 1999.

16

J S. Moore and G. Porter.
Proving properties of java threads.
(submitted for publication), 2000.

17

J. van den Berg, M. Huisman, B. Jacobs, and E. Poll.
A type-theoretic memory model for verification of sequential java programs.
In 14th International Workshop on Algebraic Development Techniques (WADT'99), volume LNCS 1827, page (to appear). Springer, 2000.

18

Matthew Wilding.
A mechanically verified application for a mechanically verified environment.
In Costas Courcoubetis, editor, Computer-Aided Verification - CAV '93, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
See URL ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/wilding-cav93.ps.

19

Matthew Wilding, David Greve, and David Hardin.
Efficient simulation of formal processor models.
Formal Methods in System Design, to appear.
Draft TR available as https://pobox.com/users/hokie/docs/efm.ps.