jStar: Towards Practical Verification for Java
In this paper we introduce a novel methodology for verifying a large set of Java programs which builds on recent theoretical developments in program veri. cation: it combines the idea of abstract predicate families [24-26] and the idea of symbolic execution and abstraction using separation logic [9]. The proposed technology has been implemented in a new automatic veri. cation system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate the effectiveness of our methodology by using jStar to verify example programs implementing four popular design patterns (subject/observer, visitor, factory, and pooling). Although these patterns are extensively used by object-oriented developers in real-world applications, so far they have been highly challenging for existing object-oriented veri. cation techniques.
verification separation logic design patterns languages theory modularity classes