javapathfinder

O JPF é um framework de análise de software extensível para bytecode Java. O jpf-core é a base para todos os projetos JPF; você sempre precisa instalá-lo. Ele contém a VM básica e a infraestrutura de verificação de modelo, e pode ser usado para verificar defeitos de concorrência, como deadlocks, e exceções não tratadas, como NullPointerExceptions e AssertionErrors.