NASA's Java PathFinder
Now this looks interesting:
Java PathFinder (JPF) is a system to verify executable Java bytecode programs. In its basic form, it is a Java Virtual Machine (JVM) that is used as an explicit state software model checker, systematically exploring all potential execution paths of a program to find violations of properties like deadlocks or unhandled exceptions. Other than traditional debuggers, JPF reports the whole execution path that leads to a defect. JPF is especially suitable to find hard-to-test concurrency defects in multithreaded programs.
Something to add to the must-look-at list!