Proving Theorems about Java-like Byte Code

J Strother Moore

- full paper
`tjvm.lisp`

: This script corresponds to the section of the paper `Specification of the TJVM'.`examples.lisp`

: This script contains all the lemmas and theorems mentioned in the paper.

You should download each of the two script files onto some directory. You may simply read them to see the definitions and theorems.

But if you wish to replay the proofs and inspect the output or
experiment with further theorems, you should certify both books with
ACL2. Certification directions are included at the top of each file.
The directions require that you edit your copy of
`examples.lisp`

so that the `include-book`

command at the beginning refers to the full pathname of your copy of
`tjvm.lisp`

.