This paper presents initial results in model checking multi-threaded
Java programs.  Java programs are translated into the SAL (Symbolic
Analysis Laboratory) intermediate language, which supports dynamic
constructs such as object instantiations and thread call stacks.  The
SAL model checker then exhaustively checks the program description for
deadlocks and assertion failures.  Basic model checking optimizations
that help curb the state explosion problem have been implemented.  To
deal with large Java programs in practice, however, supplementary
program analysis tools must work in conjunction with the model checker
to make verification manageable.  The SAL language framework provides
a good starting point to interface new and existing analysis methods
with the model checker.