An overview of JML tools and applications

Download: PDF, PostScript.

“An overview of JML tools and applications” by Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. Software Tools for Technology Transfer, vol. 7, no. 3, June 2005, pp. 212-232.
A previous version appeared in Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), (Trondheim, Norway), June 5-7, 2003.
A previous version appeared as University of Nijmegen Dept. of Computer Science technical report NIII-R0309, Mar. 2003.


The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification type-checking, runtime debugging, static analysis, and verification.

This paper gives an overview of the main ideas behind JML, details about JML's wide range of tools, and a glimpse into existing applications of JML.

Download: PDF, PostScript.

BibTeX entry:

   author = {Lilian Burdy and Yoonsik Cheon and David Cok and Michael D.
	Ernst and Joe Kiniry and Gary T. Leavens and K. Rustan M. Leino
	and Erik Poll},
   title = {An overview of {JML} tools and applications},
   journal = {Software Tools for Technology Transfer},
   volume = {7},
   number = {3},
   pages = {212--232},
   month = jun,
   year = {2005}

(This webpage was created with bibtex2web.)

Back to Program Analysis Group publications.