OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
This provides a practical verification tool for Java developers and educators, but it is incremental as it builds on existing foundations like JML and OpenJDK.
The authors tackled the problem of verifying Java programs by developing OpenJML, a tool that integrates JML, OpenJDK, and Eclipse to check code and specifications, and it has been used in college courses and small-scale studies.
OpenJML is a tool for checking code and specifications of Java programs. We describe our experience building the tool on the foundation of JML, OpenJDK and Eclipse, as well as on many advances in specification-based software verification. The implementation demonstrates the value of integrating specification tools directly in the software development IDE and in automating as many tasks as possible. The tool, though still in progress, has now been used for several college-level courses on software specification and verification and for small-scale studies on existing Java programs.