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

The work

TitleOpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
AuthorsDavid R. Cok
Typearticle
Year2014
Citekeycok2014openjml

Where it appeared

Published inElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume149
Pages79--92

Identifiers

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.

Copy held

KindPDF, 209.4 kB
Retrieved2026-08-06
Heldlocal, for personal reference
Where it came fromhttps://arxiv.org/pdf/1404.6608

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Standingendorsed
Approved2026-08-06
In: Electronic Proceedings in Theoretical Computer Science venue

Cite it as

@article{cok2014openjml,
  title = {OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse},
  author = {David R. Cok},
  year = {2014},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = {149},
  pages = {79--92},
  publisher = {Open Publishing Association},
  doi = {10.4204/eptcs.149.8},
  url = {https://arxiv.org/pdf/1404.6608},
}

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