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

The work

AuthorsDavid R. Cok
Editors
Typearticle
Year2014
Citekeycok2014openjml

Where it appeared

Published inFormal Integrated Development Environment 2014 (F-IDE 2014)
PublisherOpen Publishing Association
SeriesElectronic Proceedings in Theoretical Computer Science
Volume149
Pages79--92

Identifiers

arXiv1404.6608 from its oa_pdf_url
DOI10.4204/eptcs.149.8
OpenAlexW2029495398

Access

Landing pagehttps://doi.org/10.4204/eptcs.149.8
Free full texthttps://arxiv.org/pdf/1404.6608

Abstract

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.

A copy is held

pdf, 204.5 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-17 14:03 UTC

Filed under

cok eptcs verifying-real-java what-one-proves-with

Cite it as

@article{cok2014openjml,
  title        = {OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse},
  author       = {David R. Cok},
  year         = {2014},
  journal      = {Formal Integrated Development Environment 2014 (F-IDE 2014)},
  publisher    = {Open Publishing Association},
  series       = {Electronic Proceedings in Theoretical Computer Science},
  volume       = {149},
  pages        = {79--92},
  doi          = {10.4204/eptcs.149.8},
}

This record lives at https://refs.drheap.org/cok2014openjml/ and will keep doing so.