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:
- A (general) theorem prover for separation logic tailored to object-oriented verification. The prover embeds an abstraction module for defining abstract interpretations.
- A (general) symbolic execution module for separation logic tailored to object-oriented verification.
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
To just try the tools, you may also use the following tarballs, which contain the source code, tests, examples, and documentation.
- User's Mailing List
- MultiStar, part of EVE: an Eiffel front-end with support for multiple inheritance
- lstar: an automatic prover for programs written in bitcode
- jabstr: a jStar plugin for numerical abstractions
- TopStar, soon to join the TOPL tools: a verifier for temporal properties
- Mike Dodds (Cambridge University)
- Radu Grigore (Queen Mary, University of London)
- Rasmus Petersen (Queen Mary, University of London)
- Matko Botincan (Cambridge University)
- Dominik Gabi (Queen Mary University of London)
- Thomas Turk (Cambridge University)
- Daiva Naudziuniene (Cambridge University)