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.

This is NASA's first program to be actively developed and hosted on SourceForge, licensed under the 'NASA Open Source Agreement'.

Something to add to the must-look-at list!