SpinJa Promela Compiler 0.9
A Java-based model checker for Promela
You will be able to use SpinJa Promela Compiler to check for the absence of deadlocks, assertions, liveness properties and LTL properties (via never claims). SpinJa verification mode can use (nested) depth first search or breadth first search.
SpinJa Promela Compiler is cross-platform and it works on Mac OS X, Windows and Linux.