index.html

---
layout: home
title: Home | OpenJML  
---
  <!-- Example row of columns --> 
  <div class="row">
    <div class="col-md-4">
      <h2>Verify Your Java Programs with JML</h2>
      <p>The <a href="http://www.jmlspecs.org">Java Modeling Language</a> (JML) is a mature program specification language with more than 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
implementation (in Java) satisfies its specification (in JML).  OpenJML can also
perform runtime-assertion-checking.</p>
<p>
The goal of the OpenJML project is to implement a full tool for JML and current Java that is easy for practitioners 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.
</p>
<p><b>To learn more, select one of the menu buttons at the top of this web page.</b></p>
    </div>
    <div class="col-md-4">
      <h2>Support for Static and Runtime Checking</h2>
      <p>Verification in OpenJML can be performed either by using our static deductive 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.  </p>
<p><b>To learn more, select one of the menu buttons at the top of this web page.</b></p>
    </div>
    <div class="col-md-4">
        <h2>Command-line and IDEs</h2>
        <p>
        OpenJML is both a command-line tool and, by means of the Language Server Protocol, can be integrated into IDEs.
        That integration then enables manipulating JML specifications in a program just as you might edit text in any other programming language.
        In particular, the OpenJML project has created an <a href="documentation/openjml-eclipse.html">Eclipse plugin</a> and a 
        <a href="documentation/openjml-vscode.html">VSCode extension</a> as clients that work with the OpenJML LSP-compliant server.
        See the <a href="documentation">documentation</a> page for more information.
</p><p>
    The project's development home is <a href="https://github.com/OpenJML/OpenJML">GitHub</a>.
</p>

<!--
      <h2>Integrates with Most Popular SMT Solvers</h2>
      <p>OpenJML is not a theorem prover or model checker itself. OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. OpenJML supports uses major  SMT solvers such as Z3 and CVC5. The success of the proofs will depend on the capability of the SMT solver, the particular logical encoding of the code+specifications, and the complexity and style in which the code and specifications are written.</p>
<p><b>To learn more, select one of the menu buttons at the top of this web page.</b></p>
-->


    </div>


  </div>