``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 https://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 https://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.