By the same authors

jStar: Bringing separation logic to Java

Research output: Non-textual formSoftware


  • Dino Distefano (Developer)
  • Matthew J. Parkinson (Developer)
  • Mike Dodds (Developer)
  • Radu Grigore (Developer)
  • Rasmus Petersen (Developer)
  • Matko Botincan (Developer)
  • Dominik Gabi (Developer)
  • Thomas Turk (Developer)
  • Daiva Naudziuniene (Developer)
  • Stephen van Staden (Developer)
  • Adam Wright (Developer)


Publication details

DatePublished - 2011
Original languageEnglish


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.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations