Does your program do what it is supposed to do?

Verify Your Java Programs with JML

The Java Modeling Language (JML) is a mature program specification language with nearly two decades of history. OpenJML is capable of checking Java programs annotated with specifications in the Java Modeling Language and provides robust support for many of JML's features. That is, OpenJML does deductive program verification to check that a program's implmentation (in Java) satisfies its specification (in JML).

The goal of the OpenJML project is to implement a full tool for JML and current Java that is easy for practioners and students to use to specify and verify Java programs. In addition, the project seeks to advance the theory and experience of software verification in practical, industrially-relevant contexts.

To learn more, select one of the menu buttons at the top of this web page.

Support for Static and Runtime Checking

Verification in OpenJML can be performed either by using our static ideductive verification capability or by using our runtime assertion checking features. Runtime assertion checking is often easier to write specifications for whereas static checking gives stronger guarantees about program behavior.

To learn more, select one of the menu buttons at the top of this web page.

Though the project's development home is now GitHub, we were on SourceForge for many years; our Eclipse plug-in will be there again one it is up and running. SourceForge recognized the project as an active download site.