SpinJa Promela Compiler 0.9

SpinJa Promela Compiler is a free and open-source model checker for Promela, written in Java. Promela is the modelling language for the SPIN model checker. SpinJa supports a large subset of the Promela language.

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.

Requirements:

· Java