PathFinder

Extensible software model checker for Java bytecode. Acts as a JVM that systematically explores execution paths to find deadlocks, unhandled exceptions, and other defects; reports full paths to failures. Well-suited to concurrency bugs in multithreaded code.