Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
jStar: bringing separation logic to Java
[go: Go Back, main page]
jStar: bringing separation logic to Java.

jStar is a higly-customizable 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.

    Distribution

    jStar is distributed under a three clause BSD license. The distribution contains the source code and a complete set of examples programs.

    Download jStar

    Papers

  • jStar: Towards Practical Verification for Java. Dino Distefano and Matthew Parkinson. In OOPSLA 2008, pp. 213-226, ACM.

    People

    The people behind jStar are

  • Dino Distefano
  • Matthew Parkinson

    Contact

    For more info on jStar please contact Dino Distefano or Matthew Parkinson