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.
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 language | English |
---|---|
Publication status | Published - 2011 |