Projects built on OpenJML

OpenJML has been the foundation for a number of projects. Some of them I'm told about, some I hear about long after, and some I probably never hear about. Here are some that have provided references.

Projects built on OpenJML
  • Past expression: encapsulating pre-states at post-conditions by means of AOP. Jooyong Yi, Robby, Xianghua Deng, Abhik Roychoudhury AOSD '13 Proceedings of the 12th annual international conference on Aspect-oriented software development, 2013
  • Expressing and Checking Intended Changes via Software Change Contracts. Jooyong Yi, Dawei Qi, Shin Hwei Tan, Abhik Roychoudhury ISSTA '13 Proceedings of International Symposium on Software Testing and Analysis, 2013
  • Michael Keating, Adrian Kostrubiak and Tim Wahls. Enhancing the jmle Tool. Proceedings of the 26th Annual Conference of The Pennsylvania Association of Computer and Information Science Educators (PACISE). 15 - 21. April 8 - 9, 2011. Shippensburg University, Shippensburg, PA.
  • The JMLUnitNG project

Papers related to OpenJML

Papers Related to JML

The following papers are related to JML, but are also concerned with other matters (typically semantics of formal methods or tool support). They are listed in (approximately) reverse chronological order. Note that JML's syntax and semantics may be different from that used in older papers. You should consult the latest documentation for current details.

If you have a paper related to JML that does not appear here, we'd like to include it. Just send a citation for your paper (in XHTML, please, with links for each author and a link to a PDF file) to Gary Leavens (

Bibtex entries for the papers on this page are available from the Collection of Computer Science Bibliographies or from Gary Leavens's bibliographies. If your paper's bibtex entry is inaccurate or not available from these sources, then please send it (in bibtex format!) to Gary Leavens (