A static checker for specifications written in the Java Modeling Language. Only supports a subset of Java 7.