[separation logic] jStar: Bringing separation logic to Java

jStar: Bringing separation logic to Java Java Programに対してseparation logicを使って検証するというもので、事前事後条件を与えると、ループ不変条件は自動的に計算してくれるらしい（"Loop invariants are computed automatically by means of abstract interpretation. "） 論文(PDF)：jStar: Towards Practical Verification for Java チュートリアル(PDF): How to Verify Java Program with jStar: a Tutorial