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.
Distribution
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.
Documentation
- jStar: Towards Practical Verification for Java. Dino Distefano and Matthew Parkinson. In OOPSLA 2008, pp. 213-226, ACM.
- jStar-eclipse: an IDE for Automated Verification of Java Programs. Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore and Matthew J. Parkinson. To appear in ESEC/FSE'2011.
- coreStar: The Core of jStar. Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Daiva Naudziuniene and Matthew Parkinson. To appear in BOOGIE 2011
- Tutorial
- User's Mailing List
Other Papers
- Verification of Snapshot Isolation in Transactional Memory Java Programs. Ricardo J. Dias, Dino Distefano, João Costa Seco, João M. Lourenço. In ECOOP 2012.
- TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs. Radu Grigore, Rasmus Lerchedahl Petersen and Dino Distefano. In FOOL 2011.
Project Members
Principal investigators:
- Dino Distefano (Queen Mary, University of London)
- Matthew Parkinson
Post-docs:
- Mike Dodds (Cambridge University)
- Radu Grigore (Queen Mary, University of London)
- Rasmus Petersen (Queen Mary, University of London)
PhD students:
- Matko Botincan (Cambridge University)
- Mark Schellhase (Queen Mary University of London)
- Thomas Turk (Cambridge University)
Pre-doc:
- Daiva Naudziuniene (Cambridge University)
Collaborators:
- Stephan van Staden (ETH Zurich)
- Adam Wright (Imperial College, London)
Contact
For more info on jStar please contact Dino Distefano or Matthew Parkinson.