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.

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.