Model checking is seldom applied to implementation programs. Furthermore, when it is applied, the

usual approach is to extract relevant portions of the code, create a model of its behavior in a different

notation, and then check the latter. This approach has the drawback that it requires expertise in the

use of the model checking tools and hence will not, in general, allow software developers to check

their own code during development. In the Automated Software Engineering group at NASA Ames

we are investigating the use of model checking on actual source code in order to allow (NASA) software

developers to augment their traditional testing techniques with model checking. Here we describe our

work on applying model checking to Java programs. The first Java model checker developed within

the group, Java PathFinder 1 (JPF1), used an automatic translation from Java to PROMELA (the

input notation for the SPIN model checker) in order to do model checking. JPF1 was highly successful

in finding errors in complex Java programs since it covered a large part of the Java language, e.g.

dynamic object and thread creation, exceptions, etc. However, it could not handle language features that

were not supported by PROMELA, for example floating point numbers. Furthermore, since the tool was

based on a translation from Java to PROMELA, it required all the Java source code for a program to

be available, and this is often not the case when libraries are used. In order to solve these problems we

built a new Java model checker, JPF(2), that works directly on Java bytecode. We describe JPF's

structure and some of its novel features. Model checking often suffers from the state-explosion problem

and when checking actual source code this problem is even more acute. We use abstraction, static analysis,

and runtime analysis, in order to alleviate some of the state-explosion problems.