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

David R. Cok
(GrammaTech, Inc.)

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.

In Catherine Dubois, Dimitra Giannakopoulou and Dominique Méry: Proceedings 1st Workshop on Formal Integrated Development Environment (F-IDE 2014), Grenoble, France, April 6, 2014, Electronic Proceedings in Theoretical Computer Science 149, pp. 79–92.
Published: 26th April 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: