Re:Free download of a similar system for Java (Score 1)

The best available modern system for formal verification is the Extended Static Checking system for Java developed at DEC SRL. This was developed at DEC before HP shut down that research operation.

The problem with such a tool is its limitation to static checking. Many of the most pernicious errors are dynamic. Consider race conditions, timing skew, and deadlocks. SPARK is more than a set of tools. It is also a specification of a subset of Ada. That subset was carefully chosen to avoid many of those dynamic errors.

While Java is statically verifiable and widely used, it is also not dynamically verifiable. The performance of a Java program on a given hardware platform is highly dependent upon the particular JVM the program runs in. More than that, Java synchronization is not temporally deterministic. It is relialble on the average. Being reliable on the average is simply not good enough for many safety critical real time systems.