jStar:

Bringing separation logic to Java

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.

• jStar repository
• coreStar repository

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.

• jStar, May 2011
• coreStar, May 2011

Documentation

jStar: Towards Practical Verification for Java// Dino Distefano, Matthew Parkinson// OOPSLA 2008
jStar-eclipse: an IDE for Automated Verification of Java Programs// Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Matthew J. Parkinson// ESEC/FSE 2011
coreStar: The Core of jStar// Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Daiva Naudziuniene, Matthew J. Parkinson// BOOGIE 2011
• Tutorial
• User's Mailing List

Other Papers

Proof-Directed Parallelization Synthesis by Separation Logic// Matko Botincan, Mike Dodds, Suresh Jagannathan// TOPLAS 2013
Runtime Verification Based on Register Automata// Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos// TACAS 2013
JuS: Squeezing the Sense out of JavaScript Programs// Philippa Gardner, Daiva Naudžiuniene, Gareth Smith// JSTools 2013
Resource-Sensitive Synchronization Inference by Abduction// Matko Botincan, Mike Dodds, Suresh Jagannathan// POPL 2012
Verification of Snapshot Isolation in Transactional Memory Java Programs// Ricardo J. Dias, Dino Distefano, João Costa Seco, João M. Lourenço// ECOOP 2012
Safe Asynchronous Multicore Memory Operations// Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson// ASE 2011
Automatic Safety Proofs for Asynchronous Memory Operations// Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson// PPoPP 2011
TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs// Radu Grigore, Rasmus Lerchedahl Petersen, Dino Distefano// FOOL 2011
Verifying Executable Object-Oriented Specifications with Separation Logic// Stephan van Staden, Cristiano Calcagno, Bertrand Meyer// ECOOP 2010
Reasoning about multiple related abstractions with MultiStar// Stephan van Staden, Cristiano Calcagno// OOPSLA 2010

Successor Tools

• MultiStar, part of EVE: an Eiffel front-end with support for multiple inheritance
• JuS: a tool for analysing JavaScript programs using separation logic
• 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

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)
• Dominik Gabi (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.