`javac`

and then proving the corresponding theorem about the
JVM. Certain automatically applied strategies are implemented with rewrite
rules (and other proof-guiding pragmas) in ACL2 ``books'' to control the
theorem prover when operating on problems involving the JVM model.
- my lecture notes for the Marktoberdorf 02 Summer School
- The Apprentice Challenge, with G. Porter. The paper describes a mutual-exclusion result proved about a simple multi-threaded Java application.
`apprentice-state.lisp`

-- the Apprentice initial state (4 KB)`apprentice.lisp`

-- the Apprentice proof script (97 KB)`certify.lisp`

-- a script to re-certify all these files (4 KB)`demo.lisp`

-- a proof script for the Java recursive factorial method (20 KB)`isort.lisp`

-- a proof script for the Java insertion sort method (38 KB)`iterativedemo.lisp`

-- a proof script for the Java iterative factorial method (9 KB)`m5.lisp`

-- the M5 JVM model (101 KB)`perm.lisp`

-- some lemmas about permutations (1 KB)`universal.lisp`

-- a proof script for the ``universal program'' that can return any`int`

(10 KB)`utilities.lisp`

-- basic M5 utility lemmas (5 KB)

`apprentice.lisp`

and `utilities.lisp`

. In them you
will find `include-book`

commands that mention the standard books
`books/arithmetic/top-with-meta`

and
`books/ihs/quotient-remainder-lemmas`

. Change these pathnames to
those for your machine.
Then, while connected to the directory on which you downloaded the files,
fire up ACL2 and execute
`(ld "certify.lisp" :ld-pre-eval-print t)`

.

Recertification takes just a few minutes for all but the `apprentice`

example. That one takes about 2 hours.