Proving Theorems about Java and the JVM with ACL2

J Strother Moore

Abstract

We describe a methodology for proving theorems mechanically about Java methods. The theorem prover used is the ACL2 system, an industrial-strength version of the Boyer-Moore theorem prover. An operational semantics for a substantial subset of the Java Virtual Machine (JVM) has been defined in ACL2. Theorems are proved about Java methods and classes by compiling them with 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.

Relevant Files

Note: These files have been changed since the printed copy of the lecture notes were produced. Some definitions in m5 have been simplified with consequent changes in some statements of theorems.

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)

Recertifying

After downloading all of the files above, edit the files 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.