jStar is a highly-customisable automatic verification tool based on separation logic aiming at object-oriented programs written in Java. jStar verifies that a program meet the specifications provided by the user in the form of pre/post conditions of methods. Loop invariants are computed automatically by means of abstract interpretation.

jStar integrates two essential parts:

jStar is built on top of coreStar, a generic language independent back-end intended for building verification tools based on separation logic. coreStar can be downloaded separately from jStar.


jStar and coreStar are distributed under a three clause BSD license.

The source code is hosted on GitHub.

To set up a development environment use the following commands.

mkdir jstar; cd jstar
git clone git://github.com/seplogic/corestar.git
git clone git://github.com/seplogic/jstar.git

If you have local commits, please consider requesting a pull or letting us know on the developers mailing list.

To just try the tools, you may also use the following tarballs, which contain the source code, tests, examples, and documentation.


Other Papers

Successor Tools

Project Members

Principal investigators:


PhD students:




For more info on jStar please contact Dino Distefano or Matthew Parkinson.