OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse

OpenJML is a tool for checking code and specifications of Java programs. We describe our experi-ence 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 integrat-ing 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. 1 Introduction to OpenJML OpenJML is a tool for verification (checking consistency of code and specifications) of Java programs. It is an implementation of the Java Modeling Language (JML) [29, 32] and is built using the OpenJDK [46] compiler. OpenJML can be used both as a command-line tool and through a GUI built on Eclipse. The tool has been under development in bursts since 2009. Initially the project was simply an ex