``Formal Methods'' is the name given to the computer science research area devoted to the use of formal mathematical logic to model and analyze the properties of computing systems. One advantage of modeling a system formally is that proofs about it can be checked by mechanical proof checkers. This increases the odds that the proofs are flawless. Automated mechanical theorem provers can be used to help discover proofs, which can significantly reduce the tedium of constructing formal proofs.

This is not pie-in-the-sky formal methods proposal boilerplate. It is happening. At Advanced Micro Devices, Inc., formal models of the hardware designs for the floating-point FDIV instruction on the AMD Athlon have been mechanically proved to be compliant with the IEEE-754 standard. Indeed, all of the elementary floating-point operations on the Athlon (including addition, subtraction, multiplication, division, and square root) have been so proved. Important security properties of the IBM 4758 secure co-processor were mechanically verified at IBM Yorktown. The correctness of an auditor that checks the output of a compiler for safety-critical trainborn real-time control software for Union Switch and Signal was mechanically proved. A bit- and cycle-accurate model of a Motorola digital signal processor was mechanically proved to conform to a higher-level sequential view in which the pipeline was abstracted away - provided the microcode being executed was free of a well-defined set of hazards. Several microcoded DSP algorithms extracted from the ROM of that microprocessor were mechanically proved correct. These applications, and others, are described in [12]. All were modeled and verified using one theorem proving system, ACL2.

ACL2 [13] stands for ``A Computational Logic for Applicative Common Lisp.'' It is a functional programming language, a first-order mathematical logic, and a mechanical theorem prover. ACL2 was written by Matt Kaufmann and J Strother Moore (an author of this paper) and is the successor of the Boyer-Moore theorem prover Nqthm [3,5].

As a programming language, ACL2 is a version of Common Lisp. It provides the
familiar Lisp data objects, including numbers, strings, symbols and lists,
along with if-then-else and function application, including recursion. ACL2
is axiomatically described. For example, it is an axiom that `(IF x y
z)` is `z` if `x` is `NIL`, and is `y` otherwise. Another
axiom is that `(car (cons x y))` is `x`. Theorems about ACL2
functions can be proved in this logic, most often by case analysis,
simplification, and mathematical induction. A mechanical tool has been built
to help the human user construct proofs. This interactive computer program
combines term rewriting, decision procedures and a wide variety of heuristic
techniques to provide a symbolic manipulation system. The system has
sophisticated automatic search strategies for finding certain kinds of proofs
and those strategies can be informed and guided by advice from the user, most
often in the form of key lemmas suggested by the user and proved by the
system. For details, see [13] and the ACL2 Web site
`http://www.cs.utexas.edu/users/moore/acl2`. In this paper we
avoid ACL2 syntax and knowledge of ACL2 insofar as possible.

The techniques for modeling microprocessors and programming languages in such
a logic have been developed over a long period of time in the Boyer-Moore
community. A tour de force of the method is presented in the so-called CLI
Stack (produced by Computational Logic, Inc.)
[1,8,18] which is a hierarchy of verified components
including a microprocessor, loader, linker, assembler, two compilers, an
operating system and some applications programs, all quite simple but also
actually fabricated and practical, and all of which have been formally
specified and mechanically proved correct. Another example is the work of
Yuan Yu, in which the Motorola 68020 microprocessor is formalized. Yu's work
is sufficiently accurate that it is possible to compile 21 of the 22 programs
in the Berkeley C String Library, using `gcc -o`, and run the resulting
binaries on the formal model, computing the expected results. Furthermore,
Yu formally specified what these 21 programs were supposed to do and used the
Boyer-Moore theorem prover to prove mechanically that the binaries met the
specifications [6]. For an introduction to the modeling and proof
methods used in these projects, see [4]. We merely hint at the
techniques as we briefly describe our model of the JVM.

Of particular historical importance to the present work is Rich Cohen's ACL2 model of a single-threaded JVM [7]. The so-called ``defensive JVM'' is an accurate and complete model of a subset of the JVM instruction set. As such, the machine is more complicated than the one discussed here, but does not support threads. The defensive JVM checks the dynamic conditions required to insure type safety and is an essential step toward the specification and verification of the Java bytecode verifier. Both Cohen's model and ours are based largely on the Sun Microsystems documentation for Java and the JVM [14,9], informed by private conversations with experts and experience with Java and the JVM.

Also of special interest is the fact that the JEM1 microprocessor, the world's first silicon JVM, built by Rockwell Collins, was modeled formally with ACL2 [19,11]. Some proofs were done with the model but its primary use was as a simulator. The ACL2 model executes at about 90% of the speed of a carefully-written C simulator for the same model. The issues involved in the efficient execution of ACL2 models are discussed in the article by Greve, Wilding, and Hardin (Chapter 8) of [12].

There is a large body of academic work on Java modeling but relatively little
that is truly formal and still less that is supported by mechanized tools. A
wonderful exception is the work by Nelson, Leino and others at Compaq Systems
Research Center on the ``Extended Static Checker'' for Java, which is formal,
practical and mechanized. See
`http://research.compaq.com/SRC/esc/`. The work of Borger and
Schulte [2] on Java exceptions is quite formal and accurate, but
not supported by mechanized proofs. Mechanically checked proofs about simple
Java programs have been constructed with several theorem provers, including
HOL, Isabelle, and PVS. See, for example, [17]. However, we are
unaware of mechanically checked proofs (other than those reported here) of
Java classes that use multi-threading. Our work is distinguished primarily
by being cast in a formally defined operational (and executable) semantics.
Because we formalize the semantics we can prove theorems about the model, not
just about particular Java methods or classes. We know of no mechanically
checked proofs (ours included) of correctness properties of significant Java
applications; the field is still in its infancy.