jStar: Bringing separation logic to Java

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)

Research output: Non-textual formSoftware

Abstract

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.
Original languageEnglish
Publication statusPublished - 2011

Cite this