Java Checker is similar to traditional model checkers, except that it works directly on Java programs, rather than on models of programs. (Also, the search algorithm currently implemented in Java Checker is geared towards checking of safety properties, not liveness properties, while most model checkers can check both kinds of properties.)
The underlying theoretical framework and major design decisions in the implementation are described in the paper Model-Checking Multi-Threaded Distributed Java Programs.
We are currently implementing our state-space reduction techniques in Java PathFinder. Development of Java Checker is therefore suspended for now.